Commit 714ea4ca authored by phlo's avatar phlo

renamed Schedule to Trace

parent db851ad6
......@@ -35,7 +35,7 @@ SRC = boolector.cc \
encoder_smtlib_relational.cc \
instruction.cc \
program.cc \
schedule.cc \
trace.cc \
shell.cc \
simulator.cc \
solver.cc \
......
......@@ -28,7 +28,7 @@ void print_usage_main (const char * name)
"available commands:" << eol <<
" help print help for a specific <command>" << eol <<
" simulate simulate concurrent programs" << eol <<
" replay reevaluates a given schedule" << eol <<
" replay reevaluates a given trace" << eol <<
" solve solve concurrent programs using SMT" << eol;
}
......@@ -44,18 +44,18 @@ void print_usage_simulate (const char * name)
eol << eol <<
" -k bound execute a maximum of <bound> steps" << eol <<
" -s seed random number generator's seed" << eol <<
" -v verbose schedule output" << eol <<
" -v verbose trace output" << eol <<
" program one ore more source files, each being executed as a separate thread" << eol;
}
void print_usage_replay (const char * name)
{
std::cout << "usage: " << name <<
" replay [-k <bound>] [-v] <schedule>" <<
" replay [-k <bound>] [-v] <trace>" <<
eol << eol <<
" -k bound execute a maximum of <bound> steps" << eol <<
" -v verbose schedule output" << eol <<
" schedule the schedule to replay" << eol;
" -v verbose trace output" << eol <<
" trace the trace to replay" << eol;
}
void print_usage_solve (const char * name)
......@@ -199,12 +199,12 @@ int simulate (const char * name, const int argc, const char ** argv)
}
// run program with given seed
Schedule::ptr schedule = Simulator::simulate(programs, bound, seed);
Trace::ptr trace = Simulator::simulate(programs, bound, seed);
// print the result
std::cout << schedule->print();
std::cout << trace->print();
return schedule->exit;
return trace->exit;
}
//------------------------------------------------------------------------------
......@@ -214,7 +214,7 @@ int simulate (const char * name, const int argc, const char ** argv)
int replay (const char * name, const int argc, const char ** argv)
{
bound_t bound = 0;
std::string schedule_path;
std::string trace_path;
for (int i = 0; i < argc; i++)
{
......@@ -244,30 +244,30 @@ int replay (const char * name, const int argc, const char ** argv)
}
else
{
schedule_path = arg;
trace_path = arg;
}
}
if (schedule_path.empty())
if (trace_path.empty())
{
print_error("no schedule given");
print_error("no trace given");
print_usage_replay(name);
return -1;
}
try
{
// create and parse schedule
Schedule::ptr schedule =
std::make_unique<Schedule>(create_from_file<Schedule>(schedule_path));
// create and parse trace
Trace::ptr trace =
std::make_unique<Trace>(create_from_file<Trace>(trace_path));
// run given schedule
schedule = Simulator::replay(*schedule, bound);
// run given trace
trace = Simulator::replay(*trace, bound);
// print the result
std::cout << schedule->print();
std::cout << trace->print();
return schedule->exit;
return trace->exit;
}
catch (const std::exception & e)
{
......
......@@ -28,7 +28,7 @@ Simulator::Simulator (const Program::List::ptr & p,
const bound_t b,
const uint64_t s) :
programs(p),
schedule(std::make_unique<Schedule>(p)),
trace(std::make_unique<Trace>(p)),
bound(b),
seed(s)
{
......@@ -81,7 +81,7 @@ void Simulator::check_and_resume (word_t id)
// Simulator::run --------------------------------------------------------------
Schedule::ptr Simulator::run (std::function<Thread *()> scheduler)
Trace::ptr Simulator::run (std::function<Thread *()> scheduler)
{
assert(active.empty());
......@@ -94,7 +94,7 @@ Schedule::ptr Simulator::run (std::function<Thread *()> scheduler)
bool done = active.empty();
while (!done && (!bound || schedule->bound < bound))
while (!done && (!bound || trace->bound < bound))
{
Thread * thread = scheduler();
......@@ -166,14 +166,14 @@ Schedule::ptr Simulator::run (std::function<Thread *()> scheduler)
}
}
return move(schedule);
return move(trace);
}
// Simulator::simulate ---------------------------------------------------------
Schedule::ptr Simulator::simulate (const Program::List::ptr & programs,
const bound_t bound,
const bound_t seed)
Trace::ptr Simulator::simulate (const Program::List::ptr & programs,
const bound_t bound,
const bound_t seed)
{
Simulator simulator {programs, bound, seed};
......@@ -197,15 +197,15 @@ Schedule::ptr Simulator::simulate (const Program::List::ptr & programs,
// Simulator::replay -----------------------------------------------------------
Schedule::ptr Simulator::replay (const Schedule & schedule, const bound_t bound)
Trace::ptr Simulator::replay (const Trace & trace, const bound_t bound)
{
Simulator simulator {
schedule.programs,
bound && bound < schedule.bound ? bound : schedule.bound
trace.programs,
bound && bound < trace.bound ? bound : trace.bound
};
// replay scheduler
Schedule::iterator iterator = schedule.begin();
Trace::iterator iterator = trace.begin();
return simulator.run([&simulator, &iterator] {
if (iterator->flush)
......@@ -291,7 +291,7 @@ void Thread::flush ()
state = Thread::State::running;
simulator.heap[buffer.address] = buffer.value;
simulator.schedule->push_back(id, {buffer.address, buffer.value});
simulator.trace->push_back(id, {buffer.address, buffer.value});
}
// Thread::execute -------------------------------------------------------------
......@@ -310,7 +310,7 @@ void Thread::execute ()
}
#define PUSH_BACK_ATOMIC(pc, heap) \
simulator.schedule->push_back( \
simulator.trace->push_back( \
id, \
pc, \
accu, \
......@@ -456,7 +456,7 @@ void Thread::execute (const Instruction::Mem & m)
void Thread::execute (const Instruction::Cas & c)
{
std::optional<Schedule::Heap> heap;
std::optional<Trace::Heap> heap;
if (mem == load(c.arg, c.indirect))
{
......@@ -490,7 +490,7 @@ void Thread::execute (const Instruction::Halt & h [[maybe_unused]])
void Thread::execute (const Instruction::Exit & e)
{
simulator.schedule->exit = e.arg;
simulator.trace->exit = e.arg;
state = State::exited;
PUSH_BACK(pc);
......
......@@ -12,7 +12,7 @@
// TODO: forward-declare
#include "program.hh"
#include "schedule.hh"
#include "trace.hh"
//==============================================================================
// Simulator class
......@@ -28,9 +28,9 @@ struct Simulator
//
Program::List::ptr programs;
// generated schedule
// generated trace
//
Schedule::ptr schedule;
Trace::ptr trace;
// bound
//
......@@ -90,21 +90,21 @@ struct Simulator
// run the simulator, using the specified scheduler
//
Schedule::ptr run (std::function<Thread *()> scheduler);
Trace::ptr run (std::function<Thread *()> scheduler);
//----------------------------------------------------------------------------
// public functions
//----------------------------------------------------------------------------
// runs the simulator using a random schedule
// runs the simulator using a random trace
//
static Schedule::ptr simulate (const Program::List::ptr & programs,
bound_t bound = 0,
uint64_t seed = 0);
static Trace::ptr simulate (const Program::List::ptr & programs,
bound_t bound = 0,
uint64_t seed = 0);
// replay the given schedule (schedule must match simulator configuration)
// replay the given trace (trace must match simulator configuration)
//
static Schedule::ptr replay (const Schedule & schedule, bound_t bound = 0);
static Trace::ptr replay (const Trace & trace, bound_t bound = 0);
};
//==============================================================================
......
......@@ -10,11 +10,9 @@
// Solver::parse_attribute -----------------------------------------------------
bound_t Solver::parse_attribute (
std::istringstream & line,
bound_t Solver::parse_attribute (std::istringstream & line,
const std::string & name,
const char delimiter
)
const char delimiter)
{
std::string token;
......@@ -58,24 +56,22 @@ bool External::sat (const std::string & input)
// External::solve -------------------------------------------------------------
Schedule::ptr External::solve (Encoder & formula,
const std::string & constraints)
Trace::ptr External::solve (Encoder & formula, const std::string & constraints)
{
std::string input = build_formula(formula, constraints);
sat(input);
std::unique_ptr<Schedule> s = build_schedule(formula.programs);
std::unique_ptr<Trace> s = build_trace(formula.programs);
return s;
// return build_schedule(formula.programs);
// return build_trace(formula.programs);
}
// External::build_schedule ----------------------------------------------------
// External::build_trace -------------------------------------------------------
Schedule::ptr
External::build_schedule (const Program::List::ptr & programs)
Trace::ptr External::build_trace (const Program::List::ptr & programs)
{
// not really needed
if (!std_out.rdbuf()->in_avail())
......@@ -87,7 +83,7 @@ External::build_schedule (const Program::List::ptr & programs)
// if (!(std_out >> sat) || sat != "sat")
// runtime_error("formula is not sat [" + sat + "]");
Schedule::ptr schedule = std::make_unique<Schedule>(programs);
Trace::ptr trace = std::make_unique<Trace>(programs);
// current line number
size_t lineno = 2;
......@@ -109,34 +105,34 @@ External::build_schedule (const Program::List::ptr & programs)
switch (variable->type)
{
case Variable::Type::THREAD:
schedule->insert_thread(
trace->insert_thread(
variable->step,
variable->thread);
break;
case Variable::Type::EXEC:
schedule->insert_pc(
trace->insert_pc(
variable->step,
variable->thread,
variable->pc);
break;
case Variable::Type::ACCU:
schedule->insert_accu(
trace->insert_accu(
variable->step,
variable->thread,
variable->val);
break;
case Variable::Type::MEM:
schedule->insert_mem(
trace->insert_mem(
variable->step,
variable->thread,
variable->val);
break;
case Variable::Type::HEAP:
schedule->insert_heap(
trace->insert_heap(
variable->step,
{variable->adr, variable->val});
break;
......@@ -145,7 +141,7 @@ External::build_schedule (const Program::List::ptr & programs)
break;
case Variable::Type::EXIT_CODE:
schedule->exit = variable->val;
trace->exit = variable->val;
break;
default: {}
......@@ -158,7 +154,7 @@ External::build_schedule (const Program::List::ptr & programs)
}
}
return schedule;
return trace;
}
// External::parse_variable ----------------------------------------------------
......
......@@ -4,7 +4,7 @@
#include <memory>
#include <sstream>
#include "schedule.hh"
#include "trace.hh"
//==============================================================================
// forward declarations
......@@ -39,10 +39,10 @@ struct Solver
//
virtual bool sat (const std::string & formula) = 0;
// run solver and return schedule
// run solver and return trace
//
virtual Schedule::ptr solve (Encoder & encoder,
const std::string & constraints) = 0;
virtual Trace::ptr solve (Encoder & encoder,
const std::string & constraints) = 0;
};
//==============================================================================
......@@ -94,9 +94,9 @@ struct External : public Solver
//
virtual std::string build_command () = 0;
// build schedule based on the specific solver's output
// build trace based on the specific solver's output
//
Schedule::ptr build_schedule (const Program::List::ptr & programs);
Trace::ptr build_trace (const Program::List::ptr & programs);
virtual std::optional<Variable> parse_variable (std::istringstream & line);
......@@ -104,8 +104,7 @@ struct External : public Solver
virtual bool sat (const std::string & formula);
virtual Schedule::ptr solve (Encoder & encoder,
const std::string & constraints);
virtual Trace::ptr solve (Encoder & encoder, const std::string & constraints);
};
#endif
......@@ -51,7 +51,7 @@ 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.*
......
......@@ -17,7 +17,7 @@ struct Boolector : public ::testing::Test
::Boolector boolector;
Encoder::ptr encoder;
Program::List::ptr programs = std::make_shared<Program::List>();
Schedule::ptr schedule;
Trace::ptr trace;
};
TEST_F(Boolector, sat)
......@@ -51,18 +51,18 @@ TEST_F(Boolector, solve_check)
encoder = std::make_unique<smtlib::Functional>(programs, 16);
schedule = boolector.solve(*encoder, constraints);
trace = boolector.solve(*encoder, constraints);
/*
std::cout << "scheduled threads" << eol;
for (const auto & [step, thread] : schedule->thread_updates)
for (const auto & [step, thread] : trace->thread_updates)
{
std::cout << "\t{" << step << ", " << thread << "}" << eol;
}
std::cout << "pc updates" << eol;
unsigned long thread = 0;
for (const auto & updates : schedule->pc_updates)
for (const auto & updates : trace->pc_updates)
{
for (const auto & [step, val] : updates)
{
......@@ -73,7 +73,7 @@ TEST_F(Boolector, solve_check)
std::cout << "accu updates" << eol;
thread = 0;
for (const auto & updates : schedule->accu_updates)
for (const auto & updates : trace->accu_updates)
{
for (const auto & [step, val] : updates)
{
......@@ -83,7 +83,7 @@ TEST_F(Boolector, solve_check)
}
std::cout << "heap updates" << eol;
for (const auto & updates : schedule->heap_updates)
for (const auto & updates : trace->heap_updates)
for (const auto & [idx, val] : updates.second)
{
std::cout << "\t{" << idx << ", " << val << "}" << eol;
......@@ -111,23 +111,22 @@ TEST_F(Boolector, solve_check)
"0 3 ADDI 1 3 0 {}\n"
"0 4 STORE 0 3 0 {(0,3)}\n"
"1 1 CHECK 1 2 0 {}\n",
schedule->print());
trace->print());
std::ofstream file {"/tmp/test.schedule"};
file << schedule->print();
std::ofstream file {"/tmp/test.trace"};
file << trace->print();
file.close();
Schedule::ptr parsed =
std::make_unique<Schedule>(
create_from_file<Schedule>("/tmp/test.schedule"));
Trace::ptr parsed =
std::make_unique<Trace>(create_from_file<Trace>("/tmp/test.trace"));
std::vector<std::vector<std::pair<bound_t, word_t>>> pc_diff;
for (size_t t = 0; t < schedule->pc_updates.size(); t++)
for (size_t t = 0; t < trace->pc_updates.size(); t++)
{
std::vector<std::pair<bound_t, word_t>> diff;
std::set_symmetric_difference(
schedule->pc_updates[t].begin(), schedule->pc_updates[t].end(),
trace->pc_updates[t].begin(), trace->pc_updates[t].end(),
parsed->pc_updates[t].begin(), parsed->pc_updates[t].end(),
std::back_inserter(diff));
......@@ -146,13 +145,13 @@ TEST_F(Boolector, solve_check)
thread++;
}
ASSERT_EQ(*parsed, *schedule);
ASSERT_EQ(*parsed, *trace);
Simulator simulator (programs);
Schedule::ptr simulated (simulator.replay(*parsed));
Trace::ptr simulated (simulator.replay(*parsed));
ASSERT_EQ(*simulated, *schedule);
ASSERT_EQ(*simulated, *trace);
}
TEST_F(Boolector, DISABLED_solve_cas)
......@@ -167,7 +166,7 @@ TEST_F(Boolector, DISABLED_solve_cas)
encoder = std::make_unique<smtlib::Functional>(programs, 16);
schedule = boolector.solve(*encoder, constraints);
trace = boolector.solve(*encoder, constraints);
ASSERT_EQ(
"data/increment.cas.asm\n"
......@@ -190,7 +189,7 @@ TEST_F(Boolector, DISABLED_solve_cas)
"0 4 CAS 0 1 1 {(0,2)}\n"
"1 LOOP MEM 0 2 2 {}\n"
"1 3 ADDI 1 3 2 {}\n",
schedule->print());
trace->print());
}
TEST_F(Boolector, encode_deadlock)
......
......@@ -16,7 +16,7 @@ struct BtorMC : public ::testing::Test
::BtorMC btormc = ::BtorMC(16);
Encoder::ptr encoder;
Program::List::ptr programs = std::make_shared<Program::List>();
Schedule::ptr schedule;
Trace::ptr trace;
};
TEST_F(BtorMC, sat)
......@@ -61,18 +61,18 @@ TEST_F(BtorMC, solve_check)
encoder = std::make_unique<btor2::Encoder>(programs, 16);
schedule = btormc.solve(*encoder, constraints);
trace = btormc.solve(*encoder, constraints);
/*
std::cout << "scheduled threads" << eol;
for (const auto & [step, thread] : schedule->thread_updates)
for (const auto & [step, thread] : trace->thread_updates)
{
std::cout << "\t{" << step << ", " << thread << "}" << eol;
}
std::cout << "pc updates" << eol;
unsigned long thread = 0;
for (const auto & updates : schedule->pc_updates)
for (const auto & updates : trace->pc_updates)
{
for (const auto & [step, val] : updates)
{
......@@ -83,7 +83,7 @@ TEST_F(BtorMC, solve_check)
std::cout << "accu updates" << eol;
thread = 0;
for (const auto & updates : schedule->accu_updates)
for (const auto & updates : trace->accu_updates)
{
for (const auto & [step, val] : updates)
{
......@@ -93,7 +93,7 @@ TEST_F(BtorMC, solve_check)
}
std::cout << "heap updates" << eol;
for (const auto & updates : schedule->heap_updates)
for (const auto & updates : trace->heap_updates)
for (const auto & [idx, val] : updates.second)
{
std::cout << "\t{" << idx << ", " << val << "}" << eol;
......@@ -122,23 +122,22 @@ TEST_F(BtorMC, solve_check)
"0 4 STORE 0 3 0 {(0,3)}\n"
"1 1 CHECK 1 2 0 {}\n"
"1 2 LOAD 0 2 0 {}\n",
schedule->print());
trace->print());
std::ofstream file {"/tmp/test.schedule"};
file << schedule->print();
std::ofstream file {"/tmp/test.trace"};
file << trace->print();
file.close();
Schedule::ptr parsed =
std::make_unique<Schedule>(
create_from_file<Schedule>("/tmp/test.schedule"));
Trace::ptr parsed =
std::make_unique<Trace>(create_from_file<Trace>("/tmp/test.trace"));
std::vector<std::vector<std::pair<bound_t, word_t>>> pc_diff;
for (size_t t = 0; t < schedule->pc_updates.size(); t++)
for (size_t t = 0; t < trace->pc_updates.size(); t++)
{
std::vector<std::pair<bound_t, word_t>> diff;
std::set_symmetric_difference(
schedule->pc_updates[t].begin(), schedule->pc_updates[t].end(),
trace->pc_updates[t].begin(), trace->pc_updates[t].end(),
parsed->pc_updates[t].begin(), parsed->pc_updates[t].end(),
std::back_inserter(diff));
......@@ -157,13 +156,13 @@ TEST_F(BtorMC, solve_check)
thread++;
}
ASSERT_EQ(*parsed, *schedule);
ASSERT_EQ(*parsed, *trace);
Simulator simulator {programs};
Schedule::ptr simulated {simulator.replay(*parsed)};
Trace::ptr simulated {simulator.replay(*parsed)};
ASSERT_EQ(*simulated, *schedule);
ASSERT_EQ(*simulated, *trace);
}
TEST_F(BtorMC, DISABLED_solve_cas)
......@@ -179,7 +178,7 @@ TEST_F(BtorMC, DISABLED_solve_cas)
encoder = std::make_unique<btor2::Encoder>(programs, 16);
schedule = btormc.solve(*encoder, constraints);
trace = btormc.solve(*encoder, constraints);
ASSERT_EQ(
"",
......@@ -203,7 +202,7 @@ TEST_F(BtorMC, DISABLED_solve_cas)
// "0 4 CAS 0 1 1 {(0,2)}\n"
// "1 LOOP MEM 0 2 2 {}\n"
// "1 3 ADDI 1 3 2 {}\n",
schedule->print());
trace->print());
}
} // namespace test
......@@ -22,7 +22,7 @@ struct Instruction : public ::testing::Test
Instruction ()
{
simulator.schedule = std::make_unique<Schedule>(simulator.programs);
simulator.trace = std::make_unique<Trace>(simulator.programs);
}
};
......@@ -812,7 +812,7 @@ TEST_F(Instruction, EXIT)
ASSERT_EQ(0, thread.pc);
ASSERT_EQ(0, thread.accu);
ASSERT_EQ(1, thread.simulator.schedule->exit);
ASSERT_EQ(1, thread.simulator.trace->exit);
ASSERT_EQ(Thread::State::exited, thread.state);
}
......
......@@ -46,9 +46,9 @@ TEST_F(Main, illegal_command_line)
TEST_F(Main, simulate_increment_check)
{
// read expected schedule from file
std::ifstream schedule_file("data/increment.check.t2.k16.schedule");
std::string expected((std::istreambuf_iterator<char>(schedule_file)),
// read expected trace from file
std::ifstream trace_file("data/increment.check.t2.k16.trace");
std::string expected((std::istreambuf_iterator<char>(trace_file)),
std::istreambuf_iterator<char>());
std::string args = " simulate -v -s 0 -k 16 ";
......@@ -64,9 +64,9 @@ TEST_F(Main, simulate_increment_check)
TEST_F(Main, simulate_increment_cas)
{
// read expected schedule from file
std::ifstream schedule_file("data/increment.cas.t2.k16.schedule");
std::string expected((std::istreambuf_iterator<char>(schedule_file)),
// read expected trace from file
std::ifstream trace_file("data/increment.cas.t2.k16.trace");
std::string expected((std::istreambuf_iterator<char>(trace_file)),
std::istreambuf_iterator<char>());
std::string args = " simulate -v -s 0 -k 16 ";
......@@ -150,15 +150,15 @@ TEST_F(Main, simulate_illegal_bound)
TEST_F(Main, replay_increment_check)
{
std::string schedule_file = "data/increment.check.t2.k16.schedule";
std::string trace_path = "data/increment.check.t2.k16.trace";
// read expected schedule from file
std::ifstream sfs(schedule_file);
// read expected trace from file
std::ifstream sfs(trace_path);
std::string expected((std::istreambuf_iterator<char>(sfs)),
std::istreambuf_iterator<char>());
std::string args = " replay -v ";
std::string cmd = executable + args + schedule_file;
std::string cmd = executable + args + trace_path;
std::string actual = shell.run(cmd).str();
......@@ -168,15 +168,15 @@ TEST_F(Main, replay_increment_check)
TEST_F(Main, replay_increment_cas)
{
std::string schedule_file = "data/increment.cas.t2.k16.schedule";
std::string trace_path = "data/increment.cas.t2.k16.trace";
// read expected schedule from file
std::ifstream sfs(schedule_file);
// read expected trace from file
std::ifstream sfs(trace_path);
std::string expected((std::istreambuf_iterator<char>(sfs)),
std::istreambuf_iterator<char>());
std::string args = " replay -v ";
std::string cmd = executable + args + schedule_file;
std::string cmd = executable + args + trace_path;
std::string actual = shell.run(cmd).str();
......@@ -188,7 +188,7 @@ TEST_F(Main, replay_missing_args)
{
std::string args = " replay";
std::string expected = "error: no schedule given\n";
std::string expected = "error: no trace given\n";
std::string actual = shell.run(executable + args).str();
ASSERT_EQ(255, shell.last_exit_code());
......
This diff is collapsed.
This diff is collapsed.
......@@ -15,7 +15,7 @@ struct Z3 : public ::testing::Test
::Z3 z3;