tso_manual.h

Go to the documentation of this file.

#ifndef ILANG_MCM_TSO_MANUAL_H__
#define ILANG_MCM_TSO_MANUAL_H__

#include "ilang/mcm/memory_model.h"

namespace ilang {

class TsoTraceStep : public TraceStep {
public:
  typedef std::shared_ptr<TraceStep> TraceStepPtr;
  // ------------------------- MEMBERS -------------------------------------- //
  TraceStepPtr wfe_global; // maybe we should get away from raw pointer?
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  TsoTraceStep(const InstrPtr& inst, ZExprVec& cstr, z3::context& ctx,
               size_t pos);
}; // class TsoTraceStep

class Tso : public MemoryModel {
public:
  typedef std::shared_ptr<TsoTraceStep> TsoTraceStepPtr;
  typedef std::set<TsoTraceStepPtr> TsoTraceStepPtrSet;
  // -------------------------- TSO SELECTOR
  // -------------------------------------- //
  static InterIlaUnroller::MemoryModelCreator TsoModel;

protected:
  TraceStepPtrSet WRITE_list;
  TraceStepPtrSet READ_list;
  TraceStepPtrSet FENCE_list;
  TraceStepPtrSet RMW_list;
  TraceStepPtrSet PureWrite_list;

public:
  void virtual RegisterSteps(size_t regIdx, const InstrVec& _inst_seq) override;
  void virtual FinishRegisterSteps() override;
  void virtual ApplyAxioms() override;
  // HZ note: All the step should be registered through the first function:
  // RegisterSteps
  void virtual SetFinalProperty(const ExprPtr& property) override;

  Tso(z3::context& ctx, ZExprVec& _cstrlist, const StateNameSet& shared_states,
      const ILANameStateNameSetMap& private_states,
      const InstrLvlAbsPtr& global_ila_ptr)
      : MemoryModel(ctx, _cstrlist, shared_states, private_states,
                    global_ila_ptr) {}

private:
  z3::expr RF(const TraceStepPtr& w, const TraceStepPtr& r);
  z3::expr FR(const TraceStepPtr& r, const TraceStepPtr& w);
  z3::expr CO(const TraceStepPtr& w1, const TraceStepPtr& w2);

  // ------------------------- ACCESSOR FUNCTIONs
  // -------------------------------------- //
  static MemoryModel::TraceStepPtr
  __wfe_global(const MemoryModel::TraceStepPtr& ts);

}; // class Tso

} // namespace ilang

#endif // ILANG_MCM_TSO_MANUAL_H__