Commit b5a95a50 authored by phlo's avatar phlo

updated Simulator and Trace

* removed Thread
* added state access functions to Trace
* data generated by simulation now stored in Trace
parent b644328b
......@@ -5,6 +5,8 @@
class CVC4 : public External
{
private:
virtual std::string build_command ();
virtual std::string build_formula (Encoder & encoder,
......
......@@ -85,7 +85,7 @@ struct Model : Instruction::Concept
assert(false);
}
void execute (Thread & t) const { t.execute(pod); }
void execute (Simulator & s) const { s.execute(pod); }
std::string encode (Encoder & e) const { return e.encode(pod); }
};
......@@ -246,7 +246,7 @@ void Instruction::arg (const word_t a) { model->arg(a); }
bool Instruction::indirect () const { return model->indirect(); }
void Instruction::indirect (const bool i) { model->indirect(i); }
void Instruction::execute (Thread & t) const { model->execute(t); }
void Instruction::execute (Simulator & s) const { model->execute(s); }
std::string Instruction::encode (Encoder & e) const { return model->encode(e); }
//------------------------------------------------------------------------------
......
......@@ -39,7 +39,7 @@
// forward declarations
//==============================================================================
struct Thread;
struct Simulator;
struct Encoder;
//==============================================================================
......@@ -186,7 +186,7 @@ struct Instruction
virtual bool indirect () const = 0;
virtual void indirect (bool indirect) = 0;
virtual void execute (Thread & t) const = 0;
virtual void execute (Simulator & s) const = 0;
virtual std::string encode (Encoder & e) const = 0;
};
......@@ -241,7 +241,7 @@ struct Instruction
bool indirect () const;
void indirect (bool indirect);
void execute (Thread & t) const;
void execute (Simulator & s) const;
std::string encode (Encoder & e) const;
//----------------------------------------------------------------------------
......
This diff is collapsed.
......@@ -20,6 +20,22 @@
struct Simulator
{
//----------------------------------------------------------------------------
// member types
//----------------------------------------------------------------------------
// thread state
//
enum class State : char
{
initial = 'I', // created, but not started
running = 'R', // running
flushing = 'F', // flushing store buffer
waiting = 'W', // waiting at checkpoint
halted = 'H', // no more instructions or halted
exited = 'E' // exit called
};
//----------------------------------------------------------------------------
// members
//----------------------------------------------------------------------------
......@@ -32,6 +48,10 @@ struct Simulator
//
Trace::ptr trace;
// current step
//
size_t step;
// bound
//
size_t bound;
......@@ -40,33 +60,31 @@ struct Simulator
//
uint64_t seed;
// list of all threads
// current thread
//
std::vector<Thread> threads;
word_t thread;
// list of active threads
// list of thread states
//
// NOTE: much more lookup than insert/remove operations
//
std::vector<Thread *> active;
std::vector<State> state;
// main memory
// list of active threads
//
// address -> value
// NOTE: much more lookup than insert/remove operations
//
std::unordered_map<word_t, word_t> heap;
std::vector<word_t> active;
// number of threads containing calls to a specific checkpoint
// threads containing calls to a specific checkpoint
//
// checkpoint id -> list of threads
//
std::unordered_map<word_t, std::vector<Thread *>> threads_per_checkpoint;
std::unordered_map<word_t, std::unordered_set<word_t>> threads_per_checkpoint;
// number of threads currently waiting for a specific checkpoint
// threads waiting for a specific checkpoint
//
// checkpoint id -> number of waiting threads
// checkpoint id -> list of threads
//
std::unordered_map<word_t, word_t> waiting_for_checkpoint;
std::unordered_map<word_t, std::unordered_set<word_t>> waiting_for_checkpoint;
//----------------------------------------------------------------------------
// constructors
......@@ -84,109 +102,40 @@ struct Simulator
//
void check_and_resume (word_t id);
// creates a thread using the given program, thread id == number of threads
//
word_t create_thread (const Program & program);
// run the simulator, using the specified scheduler
//
Trace::ptr run (std::function<Thread *()> scheduler);
//----------------------------------------------------------------------------
// public functions
//----------------------------------------------------------------------------
// runs the simulator using a random trace
//
static Trace::ptr simulate (const Program::List::ptr & programs,
size_t bound = 0,
uint64_t seed = 0);
// replay the given trace (trace must match simulator configuration)
//
static Trace::ptr replay (const Trace & trace, size_t bound = 0);
};
//==============================================================================
// Thread
//==============================================================================
struct Thread
{
//----------------------------------------------------------------------------
// member types
//----------------------------------------------------------------------------
// store buffer
//
struct Buffer
{
bool full = false;
word_t address = 0;
word_t value = 0;
};
// thread state
//
enum class State : char
{
initial = 'I', // created, but not started
running = 'R', // running
flushing = 'F', // flushing store buffer
waiting = 'W', // waiting at checkpoint
halted = 'H', // no more instructions or halted
exited = 'E' // exit called
};
//----------------------------------------------------------------------------
// members
//----------------------------------------------------------------------------
// thread id
//
word_t id;
Trace::ptr run (std::function<word_t()> scheduler);
// program counter
//
word_t pc;
// special CAS register
//
word_t mem;
word_t pc () const;
void pc (word_t value);
void pc_increment ();
// accumulator register
//
word_t accu;
// current (or previous) checkpoint's id
//
word_t check;
word_t accu () const;
void accu (word_t value);
// store buffer
// special CAS register
//
Buffer buffer;
word_t mem () const;
void mem (word_t value);
// thread state
// store buffer address
//
State state;
word_t sb_adr () const;
void sb_adr (word_t value);
// reference to the simulator owning the thread
// store buffer value
//
Simulator & simulator;
word_t sb_val () const;
void sb_val (word_t value);
// reference to the program being executed
// store buffer full flag
//
const Program & program;
//----------------------------------------------------------------------------
// constructors
//----------------------------------------------------------------------------
Thread (Simulator & simulator, word_t id, const Program & program);
//----------------------------------------------------------------------------
// functions
//----------------------------------------------------------------------------
bool sb_full () const;
void sb_full (bool value);
// load value from given address
//
......@@ -197,7 +146,7 @@ struct Thread
void store (word_t address,
word_t value,
bool indirect = false,
bool atomic = false);
bool flush = false);
// flush store buffer
//
......@@ -236,12 +185,26 @@ struct Thread
void execute (const Instruction::Halt &);
void execute (const Instruction::Exit &);
//----------------------------------------------------------------------------
// public functions
//----------------------------------------------------------------------------
// runs the simulator using a random trace
//
static Trace::ptr simulate (const Program::List::ptr & programs,
size_t bound = 0,
uint64_t seed = 0);
// replay the given trace (trace must match simulator configuration)
//
static Trace::ptr replay (const Trace & trace, size_t bound = 0);
};
//==============================================================================
// non-member operators
//==============================================================================
std::ostream & operator << (std::ostream & os, Thread::State state);
std::ostream & operator << (std::ostream & os, Simulator::State state);
#endif
......@@ -52,8 +52,7 @@ GTEST_FILTER = --gtest_filter=
# GTEST_FILTER += smtlib_Relational.*
# GTEST_FILTER += btor2.*
# GTEST_FILTER += btor2_Encoder.*
# GTEST_FILTER += Thread.*
# GTEST_FILTER += Simulator.*
GTEST_FILTER += Simulator.*
# GTEST_FILTER += Main.*
# GTEST_FILTER += Experimental.*
# GTEST_FILTER += Instruction.*
......
......@@ -2,19 +2,20 @@ data/increment.cas.asm
data/increment.cas.asm
.
# tid pc cmd arg accu mem adr val full heap
0 0 STORE 0 0 0 0 0 1 {}
1 0 STORE 0 0 0 0 0 1 {}
1 0 FLUSH - 0 0 0 0 0 {(0,0)}
0 0 FLUSH - 0 0 0 0 0 {(0,0)}
1 1 FENCE - 0 0 0 0 0 {}
0 1 FENCE - 0 0 0 0 0 {}
0 2 CHECK 0 0 0 0 0 0 {}
1 2 CHECK 0 0 0 0 0 0 {}
1 LOOP MEM 0 0 0 0 0 0 {}
0 LOOP MEM 0 0 0 0 0 0 {}
0 4 ADDI 1 1 0 0 0 0 {}
0 5 CAS 0 1 0 0 0 0 {(0,1)}
0 6 JMP LOOP 1 0 0 0 0 {}
1 4 ADDI 1 1 0 0 0 0 {}
1 5 CAS 0 0 0 0 0 0 {}
1 6 JMP LOOP 0 0 0 0 0 {}
0 0 STORE 0 0 0 0 0 0 {} # 0
1 0 STORE 0 0 0 0 0 0 {} # 1
1 1 FLUSH - 0 0 0 0 1 {} # 2
0 1 FLUSH - 0 0 0 0 1 {(0,0)} # 3
1 1 FENCE - 0 0 0 0 0 {(0,0)} # 4
0 1 FENCE - 0 0 0 0 0 {} # 5
0 2 CHECK 0 0 0 0 0 0 {} # 6
1 2 CHECK 0 0 0 0 0 0 {} # 7
0 LOOP MEM 0 0 0 0 0 0 {} # 8
1 LOOP MEM 0 0 0 0 0 0 {} # 9
1 4 ADDI 1 0 0 0 0 0 {} # 10
1 5 CAS 0 1 0 0 0 0 {} # 11
1 6 JMP LOOP 1 0 0 0 0 {(0,1)} # 12
0 4 ADDI 1 0 0 0 0 0 {} # 13
0 5 CAS 0 1 0 0 0 0 {} # 14
0 6 JMP LOOP 0 0 0 0 0 {} # 15
0 LOOP MEM 0 0 0 0 0 0 {} # 16
......@@ -2,19 +2,20 @@ data/increment.check.thread.0.asm
data/increment.check.thread.n.asm
.
# tid pc cmd arg accu mem adr val full heap
0 0 STORE 0 0 0 0 0 1 {}
1 0 CHECK 0 0 0 0 0 0 {}
0 0 FLUSH - 0 0 0 0 0 {(0,0)}
0 1 FENCE - 0 0 0 0 0 {}
0 2 CHECK 0 0 0 0 0 0 {}
1 1 CHECK 1 0 0 0 0 0 {}
0 3 LOAD 0 0 0 0 0 0 {}
0 4 ADDI 1 1 0 0 0 0 {}
0 5 STORE 0 1 0 0 1 1 {}
0 6 CHECK 1 1 0 0 1 1 {}
0 7 JNZ 1 1 0 0 1 1 {}
0 7 FLUSH - 1 0 0 1 0 {(0,1)}
1 2 LOAD 0 1 0 0 0 0 {}
1 3 ADDI 1 2 0 0 0 0 {}
1 4 STORE 0 2 0 0 2 1 {}
0 1 FENCE - 1 0 0 1 0 {}
0 0 STORE 0 0 0 0 0 0 {} # 0
1 0 CHECK 0 0 0 0 0 0 {} # 1
0 1 FLUSH - 0 0 0 0 1 {} # 2
0 1 FENCE - 0 0 0 0 0 {(0,0)} # 3
0 2 CHECK 0 0 0 0 0 0 {} # 4
0 3 LOAD 0 0 0 0 0 0 {} # 5
1 1 CHECK 1 0 0 0 0 0 {} # 6
0 4 ADDI 1 0 0 0 0 0 {} # 7
0 5 STORE 0 1 0 0 0 0 {} # 8
0 6 CHECK 1 1 0 0 1 1 {} # 9
1 2 LOAD 0 0 0 0 0 0 {} # 10
1 3 ADDI 1 0 0 0 0 0 {} # 11
1 4 STORE 0 1 0 0 0 0 {} # 12
0 7 FLUSH - 1 0 0 1 1 {} # 13
0 7 JNZ 1 1 0 0 1 0 {(0,1)} # 14
0 1 FENCE - 1 0 0 1 0 {} # 15
0 2 CHECK 0 1 0 0 1 0 {} # 16
data/indirect.addressing.asm
.
# tid pc cmd arg accu mem adr val full heap
0 0 STORE 1 0 0 1 0 1 {}
0 1 ADDI 1 1 0 1 0 1 {}
0 1 FLUSH - 1 0 1 0 0 {(1,0)}
0 2 STORE [1] 1 0 0 1 1 {}
0 3 LOAD [0] 0 0 0 1 1 {}
0 4 ADD [1] 1 0 0 1 1 {}
0 5 CMP [1] 0 0 0 1 1 {}
0 0 STORE 1 0 0 1 0 1 {} # 0
0 1 ADDI 1 1 0 1 0 1 {} # 1
0 1 FLUSH - 1 0 1 0 0 {(1,0)} # 2
0 2 STORE [1] 1 0 0 1 1 {} # 3
0 3 LOAD [0] 0 0 0 1 1 {} # 4
0 4 ADD [1] 1 0 0 1 1 {} # 5
0 5 CMP [1] 0 0 0 1 1 {} # 6
......@@ -10,7 +10,8 @@
#endif
// make all class members public
#define class struct
#define private public
#define protected public
#endif // __TEST__
......
This diff is collapsed.
This diff is collapsed.
#include <gtest/gtest.h>
#include "simulator.hh"
#include "program.hh"
namespace test {
//==============================================================================
// Thread tests
//==============================================================================
struct Thread : public ::testing::Test
{
Program program;
Simulator simulator = Simulator(std::make_shared<Program::List>(1));
::Thread thread = ::Thread(simulator, 0, program);
};
// Thread::load ================================================================
TEST_F(Thread, load)
{
// direct
simulator.heap[0] = 1;
ASSERT_EQ(1, simulator.heap[0]);
ASSERT_EQ(1, thread.load(0));
// indirect
ASSERT_EQ(0, simulator.heap[1]);
ASSERT_EQ(1, thread.load(1, true));
// store buffer - direct
thread.buffer.address = 1;
thread.buffer.value = 1;
thread.buffer.full = true;
ASSERT_EQ(1, thread.load(1));
// store buffer - indirect
ASSERT_EQ(1, thread.load(0, true));
ASSERT_EQ(1, thread.load(1, true));
}
// Thread::store ===============================================================
TEST_F(Thread, store)
{
// store direct
ASSERT_EQ(0, thread.buffer.address);
ASSERT_EQ(0, thread.buffer.value);
ASSERT_FALSE(thread.buffer.full);
ASSERT_EQ(0, simulator.heap[0]);
thread.store(0, 1, false);
ASSERT_EQ(0, thread.buffer.address);
ASSERT_EQ(1, thread.buffer.value);
ASSERT_TRUE(thread.buffer.full);
ASSERT_EQ(0, simulator.heap[0]);
thread.state = ::Thread::State::flushing;
thread.flush();
ASSERT_FALSE(thread.buffer.full);
ASSERT_EQ(1, simulator.heap[0]);
// store indirect
ASSERT_EQ(0, simulator.heap[1]);
thread.store(0, 1, true);
ASSERT_EQ(1, thread.buffer.address);
ASSERT_EQ(1, thread.buffer.value);
ASSERT_TRUE(thread.buffer.full);
ASSERT_EQ(0, simulator.heap[1]);
thread.state = ::Thread::State::flushing;
thread.flush();
ASSERT_FALSE(thread.buffer.full);
ASSERT_EQ(1, simulator.heap[1]);
}
TEST_F(Thread, store_atomic)
{
// store direct
ASSERT_EQ(0, thread.buffer.address);
ASSERT_EQ(0, thread.buffer.value);
ASSERT_FALSE(thread.buffer.full);
ASSERT_EQ(0, simulator.heap[0]);
thread.store(0, 1, false, true);
ASSERT_FALSE(thread.buffer.full);
ASSERT_EQ(1, simulator.heap[0]);
// store indirect
ASSERT_EQ(0, simulator.heap[1]);
thread.store(0, 1, true, true);
ASSERT_FALSE(thread.buffer.full);
ASSERT_EQ(1, simulator.heap[1]);
}
// Thread::flush ===============================================================
TEST_F(Thread, flush)
{
thread.buffer.address = 0;
thread.buffer.value = 1;
thread.buffer.full = true;
thread.state = ::Thread::State::flushing;
ASSERT_EQ(0, simulator.heap[0]);
thread.flush();
ASSERT_EQ(1, simulator.heap[0]);
}
// Thread::execute =============================================================
TEST_F(Thread, execute)
{
// success
ASSERT_EQ(0, thread.pc);
ASSERT_EQ(0, thread.accu);
ASSERT_EQ(::Thread::State::initial, thread.state);
program.push_back(Instruction::create("ADDI", 1));
thread.execute();
ASSERT_EQ(1, thread.pc);
ASSERT_EQ(1, thread.accu);
// fail - pc > program => STOPPED
ASSERT_EQ(1, program.size());
ASSERT_EQ(::Thread::State::halted, thread.state);
try
{
thread.execute();
ASSERT_TRUE(false) << "thread stopped: expected exception";
}
catch (...) {};
ASSERT_EQ(1, thread.pc);
ASSERT_EQ(1, thread.accu);
}
} // namespace test
This diff is collapsed.
This diff is collapsed.
......@@ -23,17 +23,17 @@ struct Trace
// step -> state
//
template <typename T>
template <class T>
using update_map = std::map<size_t, T>;
// thread -> step -> state
//
template <typename T>
using thread_states = std::vector<update_map<T>>;
template <class T>
using thread_map = std::vector<update_map<T>>;
// address -> step -> state
//
using heap_states = std::unordered_map<word_t, update_map<word_t>>;
using heap_val_map = std::unordered_map<word_t, update_map<word_t>>;
// heap cell -----------------------------------------------------------------
//
......@@ -54,8 +54,8 @@ struct Trace
word_t mem;
word_t sb_adr;
word_t sb_val;
bool sb_full;
bool flush;
bool sb_full;
bool flush;
std::optional<cell_t> heap;
Step () = default;
......@@ -109,26 +109,30 @@ struct Trace
thread_state_iterators<word_t> mem;
thread_state_iterators<word_t> sb_adr;
thread_state_iterators<word_t> sb_val;
thread_state_iterators<bool> sb_full;
thread_state_iterators<bool> sb_full;
// heap update iterator
//
update_map_iterator<word_t> heap_adr;
// heap state update iterators
// heap value update iterator
//
std::unordered_map<word_t, update_map_iterator<word_t>> heap;
std::unordered_map<word_t, update_map_iterator<word_t>> heap_val;
//------------------------------------------------------------------------
// private member functions
//------------------------------------------------------------------------
// helper for initializing thread update iterator
// helper for initializing thread update iterators
//
template <typename T>
void init_iterator (thread_state_iterators<T> & iterator,
const thread_states<T> & updates);
void init_iterators (thread_state_iterators<T> & iterators,
const thread_map<T> & updates);
// return current thread state and advance
//
template <typename T>
const T & next_thread_state (update_map_iterator<T> & state);
const T & next_state (update_map_iterator<T> & updates);
// return current heap state update and advance
//
......@@ -154,7 +158,7 @@ struct Trace
// constructors
//------------------------------------------------------------------------
iterator (const Trace * trace, size_t step = 1);
iterator (const Trace * trace, size_t step = 0);
//------------------------------------------------------------------------
// member operators
......@@ -180,9 +184,9 @@ struct Trace
//
Program::List::ptr programs;
// bound used == size()
// trace length
//
size_t bound;
size_t length;
// exit code
//
......@@ -202,26 +206,32 @@ struct Trace
//
// thread -> step -> val
//
thread_states<word_t> pc_updates;
thread_states<word_t> accu_updates;
thread_states<word_t> mem_updates;
thread_states<word_t> sb_adr_updates;
thread_states<word_t> sb_val_updates;
thread_states<bool> sb_full_updates;
thread_map<word_t> pc_updates;
thread_map<word_t> accu_updates;
thread_map<word_t> mem_updates;
thread_map<word_t> sb_adr_updates;
thread_map<word_t> sb_val_updates;
thread_map<bool> sb_full_updates;
// heap state updates
//
// address -> list of (step, val) pairs
// step -> address
//
heap_states heap_updates;
update_map<word_t> heap_adr_updates;
// heap value updates
//
// address -> step -> value
//
heap_val_map heap_val_updates;
//----------------------------------------------------------------------------
// constructors
//----------------------------------------------------------------------------
// initialize with given bound
// initialize with given length
//
explicit Trace (size_t bound);
explicit Trace (size_t length);
// construct from simulator/solver
//
......@@ -237,7 +247,9 @@ struct Trace
// initialize thread state update lists
//
void init_thread_states ();
template <typename T>
void init_register_states (thread_map<T> & updates);
void init_register_states ();
// append state update helper
//
......@@ -253,11 +265,8 @@ struct Trace
word_t sb_adr,
word_t sb_val,
word_t sb_full,
const std::optional<cell_t> & heap);
// append state update after flushing the store buffer
//
void push_back (word_t thread, const cell_t & heap);
std::optional<cell_t> & heap,
bool flush = false);
// append individual state updates
//
......@@ -269,9 +278,26 @@ struct Trace
void push_back_sb_val (size_t step, word_t thread, word_t val);
void push_back_sb_full (size_t step, word_t thread, bool full);
void push_back_heap (size_t step, const cell_t & heap);
void push_back_flush (const size_t step);
void push_back_flush (size_t step);
// return most recently scheduled thread's id
//
word_t thread () const;
// return most recent register states
//
word_t pc (word_t thread) const;
word_t accu (word_t thread) const;
word_t mem (word_t thread) const;
word_t sb_adr (word_t thread) const;
word_t sb_val (word_t thread) const;
bool sb_full (word_t thread) const;
// return most recent heap state
//
word_t heap (word_t address) const;
// return trace size (bound)
// return trace size (length)
//
size_t size () const;
...