Commit 5401751d authored by phlo's avatar phlo

updated Instruction class

parent fd170d0f
......@@ -33,7 +33,7 @@ SRC = boolector.cc \
encoder_smtlib.cc \
encoder_smtlib_functional.cc \
encoder_smtlib_relational.cc \
instructionset.cc \
instruction.cc \
program.cc \
schedule.cc \
shell.cc \
......@@ -62,6 +62,11 @@ debug: build
valgrind: build
$(MAKE) -C test valgrind
# run experiments
.PHONY: experiments
experiments:
$(MAKE) -C test experiments
# build executable
.PHONY: build
build: $(MAIN)
......
#include "encoder.hh"
using namespace std;
const string Encoder::accu_sym = "accu";
const string Encoder::mem_sym = "mem";
const string Encoder::sb_adr_sym = "sb-adr";
const string Encoder::sb_val_sym = "sb-val";
const string Encoder::sb_full_sym = "sb-full";
const string Encoder::stmt_sym = "stmt";
const string Encoder::block_sym = "block";
const string Encoder::heap_sym = "heap";
const string Encoder::exit_flag_sym = "exit";
const string Encoder::exit_code_sym = "exit-code";
const string Encoder::thread_sym = "thread";
const string Encoder::exec_sym = "exec";
const string Encoder::flush_sym = "flush";
const string Encoder::check_sym = "check";
const string Encoder::cas_sym = "cas";
const string Encoder::accu_comment = "accu variables";
const string Encoder::mem_comment = "mem variables";
const string Encoder::sb_adr_comment = "store buffer address variables";
const string Encoder::sb_val_comment = "store buffer value variables";
const string Encoder::sb_full_comment = "store buffer full variables";
const string Encoder::stmt_comment = "statement activation variables";
const string Encoder::block_comment = "blocking variables";
const string Encoder::heap_comment = "heap variable";
//==============================================================================
// using declarations
//==============================================================================
using std::string;
using std::ostringstream;
//==============================================================================
// Encoder
//==============================================================================
//------------------------------------------------------------------------------
// static members
//------------------------------------------------------------------------------
const string Encoder::accu_sym = "accu";
const string Encoder::mem_sym = "mem";
const string Encoder::sb_adr_sym = "sb-adr";
const string Encoder::sb_val_sym = "sb-val";
const string Encoder::sb_full_sym = "sb-full";
const string Encoder::stmt_sym = "stmt";
const string Encoder::block_sym = "block";
const string Encoder::heap_sym = "heap";
const string Encoder::exit_flag_sym = "exit";
const string Encoder::exit_code_sym = "exit-code";
const string Encoder::thread_sym = "thread";
const string Encoder::exec_sym = "exec";
const string Encoder::flush_sym = "flush";
const string Encoder::check_sym = "check";
const string Encoder::accu_comment = "accu variables";
const string Encoder::mem_comment = "mem variables";
const string Encoder::sb_adr_comment = "store buffer address variables";
const string Encoder::sb_val_comment = "store buffer value variables";
const string Encoder::sb_full_comment = "store buffer full variables";
const string Encoder::stmt_comment = "statement activation variables";
const string Encoder::block_comment = "blocking variables";
const string Encoder::heap_comment = "heap variable";
const string Encoder::exit_flag_comment = "exit flag variable";
const string Encoder::exit_code_comment = "exit code variable";
const string Encoder::thread_comment = "thread activation variables";
const string Encoder::exec_comment = "statement execution variables";
const string Encoder::flush_comment = "store buffer flush variables";
const string Encoder::check_comment = "checkpoint variables";
const string Encoder::cas_comment = "CAS condition variables";
const string Encoder::thread_comment = "thread activation variables";
const string Encoder::exec_comment = "statement execution variables";
const string Encoder::flush_comment = "store buffer flush variables";
const string Encoder::check_comment = "checkpoint variables";
Encoder::Encoder (const Program_list_ptr p, bound_t b) :
//------------------------------------------------------------------------------
// constructors
//------------------------------------------------------------------------------
Encoder::Encoder (const Program::List::ptr & p, bound_t b) :
programs(p),
num_threads(p->size()),
bound(b),
......@@ -47,36 +62,46 @@ Encoder::Encoder (const Program_list_ptr p, bound_t b) :
iterate_programs([this] (const Program & program) {
for (pc = 0; pc < program.size(); pc++)
{
const Instruction_ptr & op = program[pc];
const Instruction & op = program[pc];
// collect statements requiring an empty store buffer
if (op->requires_flush())
if (op.requires_flush())
flush_pcs[thread].push_back(pc);
// collect checkpoints
if (Check_ptr s = dynamic_pointer_cast<Check>(op))
check_pcs[s->arg][thread].insert(pc);
// collect exit calls
if (Exit_ptr e = dynamic_pointer_cast<Exit>(op))
if (&op.symbol() == &Instruction::Exit::symbol)
exit_pcs[thread].push_back(pc);
}
// collect checkpoints
for (const auto & [c, pcs] : program.checkpoints)
{
auto & lst = check_pcs[c][thread];
// collect CAS statemets
if (Cas_ptr c = dynamic_pointer_cast<Cas>(op))
cas_threads.insert(thread);
lst.reserve(lst.size() + pcs.size());
lst.insert(lst.end(), pcs.begin(), pcs.end());
}
});
}
//------------------------------------------------------------------------------
// public member functions
//------------------------------------------------------------------------------
// Encode::str -----------------------------------------------------------------
string Encoder::str () { return formula.str(); }
/* DEBUG **********************************************************************/
//------------------------------------------------------------------------------
// DEBUG
//------------------------------------------------------------------------------
string Encoder::predecessors_to_string ()
{
ostringstream ss;
for (word_t tid = 0; tid < programs->size(); tid++)
for (const auto & [_pc, _predecessors] : programs->at(tid)->predecessors)
for (const auto & [_pc, _predecessors] : (*programs)[tid].predecessors)
{
ss << "thread " << tid << " @ " << _pc << " :";
for (const auto & prev : _predecessors)
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
#include "encoder.hh"
#include <cassert>
#include <deque>
#include "smtlib.hh"
using namespace std;
//==============================================================================
// using declarations
//==============================================================================
SMTLib_Encoder_Functional::SMTLib_Encoder_Functional (
const Program_list_ptr p,
bound_t b,
bool e
) : SMTLib_Encoder(p, b)
using std::string;
using std::vector;
//==============================================================================
// SMTLib_Encoder_Functional
//==============================================================================
//------------------------------------------------------------------------------
// constructors
//------------------------------------------------------------------------------
SMTLib_Encoder_Functional::SMTLib_Encoder_Functional (const Program::List::ptr & p,
const bound_t b,
const bool e) :
SMTLib_Encoder(p, b)
{
if (e) encode();
}
//------------------------------------------------------------------------------
// functions
//------------------------------------------------------------------------------
// SMTLib_Encoder_Functional::define_accu --------------------------------------
#define DEFINE_STATE(_update, _type, _var) \
do { \
update = _update; \
......@@ -24,15 +41,15 @@ SMTLib_Encoder_Functional::SMTLib_Encoder_Functional (
pc = program.size() - 1; \
for (auto rit = program.rbegin(); rit != program.rend(); ++rit, pc--) \
{ \
const Instruction_ptr & op = *rit; \
if (op->type() & _type) \
const Instruction & op = *rit; \
if (op.type() & _type) \
expr = \
smtlib::ite( \
exec_var(prev, thread, pc), \
op->encode(*this), \
op.encode(*this), \
expr); \
} \
formula << assign_var(_var(step, thread), expr) << eol; \
formula << assign(_var(step, thread), expr) << eol; \
}); \
formula << eol; \
} while (0)
......@@ -42,33 +59,41 @@ void SMTLib_Encoder_Functional::define_accu ()
if (verbose)
formula << accu_comment;
DEFINE_STATE(Update::accu, Types::accu, accu_var);
DEFINE_STATE(State::accu, Instruction::Type::accu, accu_var);
}
// SMTLib_Encoder_Functional::define_mem ---------------------------------------
void SMTLib_Encoder_Functional::define_mem ()
{
if (verbose)
formula << mem_comment;
DEFINE_STATE(Update::mem, Types::mem, mem_var);
DEFINE_STATE(State::mem, Instruction::Type::mem, mem_var);
}
// SMTLib_Encoder_Functional::define_sb_adr ------------------------------------
void SMTLib_Encoder_Functional::define_sb_adr ()
{
if (verbose)
formula << sb_adr_comment;
DEFINE_STATE(Update::sb_adr, Types::write, sb_adr_var);
DEFINE_STATE(State::sb_adr, Instruction::Type::write, sb_adr_var);
}
// SMTLib_Encoder_Functional::define_sb_val ------------------------------------
void SMTLib_Encoder_Functional::define_sb_val ()
{
if (verbose)
formula << sb_val_comment;
DEFINE_STATE(Update::sb_val, Types::write, sb_val_var);
DEFINE_STATE(State::sb_val, Instruction::Type::write, sb_val_var);
}
// SMTLib_Encoder_Functional::define_sb_full -----------------------------------
void SMTLib_Encoder_Functional::define_sb_full ()
{
if (verbose)
......@@ -79,13 +104,13 @@ void SMTLib_Encoder_Functional::define_sb_full ()
pc = program.size() - 1;
for (auto rit = program.rbegin(); rit != program.rend(); ++rit, pc--)
if ((*rit)->type() & Types::write)
if (rit->type() & Instruction::Type::write)
args.push_back(exec_var(prev, thread, pc));
args.push_back(sb_full_var(prev, thread));
formula <<
assign_var(
assign(
sb_full_var(),
smtlib::ite(
flush_var(prev, thread),
......@@ -96,6 +121,8 @@ void SMTLib_Encoder_Functional::define_sb_full ()
formula << eol;
}
// SMTLib_Encoder_Functional::define_stmt --------------------------------------
void SMTLib_Encoder_Functional::define_stmt ()
{
if (verbose)
......@@ -110,17 +137,19 @@ void SMTLib_Encoder_Functional::define_stmt ()
stmt_var(prev, thread, pc),
smtlib::lnot(exec_var(prev, thread, pc))});
const auto & pred = program.predecessors.at(pc);
const auto & preds = program.predecessors.at(pc);
for (auto p = pred.rbegin(); p != pred.rend(); ++p)
for (auto rit = preds.rbegin(); rit != preds.rend(); ++rit)
{
// predecessor's execution variable
string val = exec_var(prev, thread, *p);
string val = exec_var(prev, thread, *rit);
// build conjunction of execution variable and jump condition
if (Jmp_ptr j = dynamic_pointer_cast<Jmp>(program[*p]))
const Instruction & pred = program[*rit];
if (pred.is_jump())
{
string cond = j->encode(*this);
string cond = pred.encode(*this);
// JMP has no condition and returns an empty string
if (!cond.empty())
......@@ -128,22 +157,24 @@ void SMTLib_Encoder_Functional::define_stmt ()
smtlib::land({
val,
// only activate successor if jump condition failed
*p == pc - 1 && j->arg != pc
*rit == pc - 1 && pred.arg() != pc
? smtlib::lnot(cond)
: cond});
}
// add predecessor to the activation
expr = smtlib::ite(stmt_var(prev, thread, *p), val, expr);
expr = smtlib::ite(stmt_var(prev, thread, *rit), val, expr);
}
formula << assign_var(stmt_var(), expr) << eol;
formula << assign(stmt_var(), expr) << eol;
}
formula << eol;
});
}
// SMTLib_Encoder_Functional::define_block -------------------------------------
void SMTLib_Encoder_Functional::define_block ()
{
if (check_pcs.empty())
......@@ -165,7 +196,7 @@ void SMTLib_Encoder_Functional::define_block ()
block_args.push_back(block_var(prev, c, t));
formula <<
assign_var(
assign(
block_var(step, c, t),
smtlib::ite(
check_var(prev, c),
......@@ -177,12 +208,14 @@ void SMTLib_Encoder_Functional::define_block ()
formula << eol;
}
// SMTLib_Encoder_Functional::define_heap --------------------------------------
void SMTLib_Encoder_Functional::define_heap ()
{
if (verbose)
formula << heap_comment;
update = Update::heap;
update = State::heap;
const string heap_prev = heap_var(prev);
string expr = heap_prev;
......@@ -192,13 +225,13 @@ void SMTLib_Encoder_Functional::define_heap ()
for (auto rit = program.rbegin(); rit != program.rend(); ++rit, pc--)
{
const Instruction_ptr & op = *rit;
const Instruction & op = *rit;
if (op->type() & Types::atomic)
if (op.type() & Instruction::Type::atomic)
expr =
smtlib::ite(
exec_var(prev, thread, pc),
op->encode(*this),
op.encode(*this),
expr);
}
......@@ -212,11 +245,11 @@ void SMTLib_Encoder_Functional::define_heap ()
expr);
});
formula << assign_var(heap_var(), expr) << eol;
formula << eol;
formula << assign(heap_var(), expr) << eol << eol;
}
// SMTLib_Encoder_Functional::define_exit_code ---------------------------------
void SMTLib_Encoder_Functional::define_exit_flag ()
{
if (exit_pcs.empty())
......@@ -232,10 +265,11 @@ void SMTLib_Encoder_Functional::define_exit_flag ()
args.push_back(exec_var(prev, thread, exit_pc));
});
formula << assign_var(exit_flag_var(), smtlib::lor(args)) << eol << eol;
formula << assign(exit_flag_var(), smtlib::lor(args)) << eol << eol;
}
// TODO
// SMTLib_Encoder_Functional::define_exit_flag ---------------------------------
void SMTLib_Encoder_Functional::define_exit_code ()
{
if (verbose)
......@@ -250,13 +284,15 @@ void SMTLib_Encoder_Functional::define_exit_code ()
ite =
smtlib::ite(
exec_var(k, thread, exit_pc),
program[exit_pc]->encode(*this),
program[exit_pc].encode(*this),
ite);
});
formula << assign_var(exit_code_sym, ite) << eol << eol;
formula << assign(exit_code_var, ite) << eol << eol;
}
// SMTLib_Encoder_Functional::define_states ------------------------------------
void SMTLib_Encoder_Functional::define_states ()
{
assert(step);
......@@ -276,6 +312,8 @@ void SMTLib_Encoder_Functional::define_states ()
define_exit_flag();
}
// SMTLib_Encoder_Functional::encode -------------------------------------------
void SMTLib_Encoder_Functional::encode ()
{
SMTLib_Encoder::encode();
......
This diff is collapsed.
#include "instruction.hh"
#include <cassert>
#include "encoder.hh"
#include "simulator.hh"
//==============================================================================
// using declarations
//==============================================================================
using std::string;
using std::unique_ptr;
using std::make_unique;
using std::is_base_of;
using std::runtime_error;
//==============================================================================
// Instruction::Set
//==============================================================================
//------------------------------------------------------------------------------
// static members
//------------------------------------------------------------------------------
unique_ptr<Instruction::Set::nullary_t> Instruction::Set::nullary;
unique_ptr<Instruction::Set::unary_t> Instruction::Set::unary;
unique_ptr<Instruction::Set::memory_t> Instruction::Set::memory;
//------------------------------------------------------------------------------
// static member functions
//------------------------------------------------------------------------------
bool Instruction::Set::contains (const string & symbol)
{
if (nullary->find(symbol) != nullary->end())
return true;
if (unary->find(symbol) != unary->end())
return true;
if (memory->find(symbol) != memory->end())
return true;
return false;
}
template <class POD>
const string & Instruction::Set::add_nullary (const string && symbol)
{
if (!nullary)
nullary = make_unique<nullary_t>();
return
nullary->emplace(
symbol,
[] () -> Instruction { return POD(); })
.first->first;
}
template <class POD>
const string & Instruction::Set::add_unary (const string && symbol)
{
if (!unary)
unary = make_unique<unary_t>();
return
unary->emplace(
symbol,
[] (word_t a) -> Instruction { return POD(a); })
.first->first;
}
template <class POD>
const string & Instruction::Set::add_memory (const string && symbol)
{
add_unary<POD>(string {symbol});
if (!memory)
memory = make_unique<memory_t>();
return
memory->emplace(
symbol,
[] (word_t a, bool i) -> Instruction { return POD(a, i); })
.first->first;
}
Instruction Instruction::Set::create (const string & symbol)
{
if (nullary->find(symbol) == nullary->end())
throw runtime_error("Instruction '" + symbol + "' unknown");
return (*nullary)[symbol]();
}
Instruction Instruction::Set::create (const string & symbol, const word_t arg)
{
if (unary->find(symbol) == unary->end())
throw runtime_error("Instruction '" + symbol + "' unknown");
return (*unary)[symbol](arg);
}
Instruction Instruction::Set::create (const string & symbol,
const word_t arg,
const bool indirect)
{
if (memory->find(symbol) == memory->end())
throw runtime_error("Instruction '" + symbol + "' unknown");
return (*memory)[symbol](arg, indirect);
}
//==============================================================================
// Model<T>
//
// * Instruction::Concept implementation
//==============================================================================
template <class T>
struct Model : public Instruction::Concept
{
using Nullary = Instruction::Nullary;
using Unary = Instruction::Unary;
using Memory = Instruction::Memory;
T pod;
Model (const T & p) : pod(p) {}
// Model (const T && pod) : obj(move(pod)) {}
virtual pointer clone () const { return make_unique<Model<T>>(pod); }
virtual bool is_nullary () const { return is_base_of<Nullary, T>(); }
virtual bool is_unary () const { return is_base_of<Unary, T>(); }
virtual bool is_memory () const { return is_base_of<Memory, T>(); }
virtual bool is_jump () const { return pod.type & Instruction::Type::jump; }
virtual bool requires_flush () const
{
return pod.type & (Instruction::Type::write | Instruction::Type::barrier);
}
virtual const string & symbol () const { return pod.symbol; }
virtual uint8_t type () const { return pod.type; }
virtual void type (uint8_t type) { pod.type = type; }
virtual word_t arg () const { const Unary & u = *this; return u.arg; }
virtual bool indirect () const { const Memory & m = *this; return m.indirect; }
virtual void execute (Thread & t) const { t.execute(pod); }
virtual string encode (Encoder & e) const { return e.encode(pod); }
virtual operator const Unary & () const
{
assert(is_unary());
return dynamic_cast<const Unary &>(pod);
}
virtual operator const Memory & () const
{
assert(is_memory());
return dynamic_cast<const Memory &>(pod);
}
};
//==============================================================================
// Instruction
//==============================================================================
//------------------------------------------------------------------------------
// constructors
//------------------------------------------------------------------------------
template <class T>
Instruction::Instruction (const T & pod) :
model(make_unique<Model<T>>(pod))
{}
Instruction::Instruction (const Instruction & other) :
model(other.model->clone())
{}
//------------------------------------------------------------------------------
// member functions
//------------------------------------------------------------------------------
bool Instruction::is_nullary () const { return model->is_nullary(); }
bool Instruction::is_unary () const { return model->is_unary(); }
bool Instruction::is_memory () const { return model->is_memory(); }
bool Instruction::is_jump () const { return model->is_jump(); }
bool Instruction::requires_flush () const { return model->requires_flush(); }
const string & Instruction::symbol () const { return model->symbol(); }
uint8_t Instruction::type () const { return model->type(); }
void Instruction::type (uint8_t t) { model->type(t); }
word_t Instruction::arg () const { return model->arg(); }
bool Instruction::indirect () const { return model->indirect(); }
void Instruction::execute (Thread & t) const { model->execute(t); }
string Instruction::encode (Encoder & e) const { return model->encode(e); }
//------------------------------------------------------------------------------
// member operators
//------------------------------------------------------------------------------
// assignment ------------------------------------------------------------------
Instruction & Instruction::operator = (const Instruction & other)
{
model = other.model->clone();
return *this;
}
// conversion ------------------------------------------------------------------
Instruction::operator const Unary & () const { return *model; }
Instruction::operator const Memory & () const { return *model; }
//==============================================================================
// non-member operators
//==============================================================================
// equality --------------------------------------------------------------------
bool operator == (const Instruction & a, const Instruction & b)
{
if (a.symbol() != b.symbol())
return false;
if (a.type() != b.type())
return false;
if (a.is_memory() && b.is_memory())
{
const Instruction::Memory & ma = a, mb = b;
return ma.arg == mb.arg && ma.indirect == mb.indirect;
}
else if (a.is_unary() && b.is_unary())
{
const Instruction::Unary & ua = a, ub = b;
return ua.arg == ub.arg;
}
return true;
}
bool operator != (const Instruction & a, const Instruction & b)
{
return !(a == b);
}
#ifndef INSTRUCTION_HH_
#define INSTRUCTION_HH_
#include <memory>