-
Notifications
You must be signed in to change notification settings - Fork 27
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Rework ExecutionModel #732
Comments
@CapZTr as we discussed, @ThomasHaas @natgavrilenko @JonasOberhauser if you have further comments or requirements, feel free to comment |
I think the following is true:
Ideally, such an |
This is as a collection of requirements for the rework of the
ExecutionModel
class and its usages (specially generation of violation witnesses in *.graphviz format).Currently, the
ExecutionModel
is a wrapper around an SMT model representing a (not necessarily consistent) execution with an API that allows to get information in a workable manner. We need a more general class that represents executions no matter where this execution is coming from (i.e., its "source"). Some possible sources are SMT model, svcomp violation witness, violation coming from other tools like genmc.Internally, the class should contain at least
rf
)co
)It should also be able to give information about other base relations like
po
,ext
,ctrl
, ...One could explicitly store those relations (similar to
rf
andco
) or extract them using information from theEvent
class, e.g. we can check if two events belong to the same thread withEvent.getThread()
and compare ids withEvent.getGlobalId()
. This gives us all info we need to decide the program orderpo
.For dependency relations (
data
,addr
,ctrl
), it might be easier to save them explicitly (e.g., this is something the SMT solver will give us, but maybe not other sources)It should also be able to compute derive relations. Right now, if one uses
--method=eager
, derived relations can also be queried to the SMT solver model (same as for base relations).However, if one uses
--method=lazy
, the SMT solver only knows about base relations. TheWMMSolver
will construct aExecutionGraph
from theExecutionModel
which populates the graph representation of derived relations.The new
ExecutionModel
should definitely be able to populate itself from an SMT model, but the design should be flexible enough to eventually rewrite the code in/home/ponce/git/Dat3M/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml
to use theExecutionModel
. The default--method
iseager
, so the solution should definitely be able to populate the derived relations from the SMT model information of base ones.Right now,
ExecutionModel
only keep track of memory events (loads and stores). The new class should also keep track of other events (at leastLocal
since those help to debug low level data flow). Control-flow events likeCondJump
andLabel
can probably be skipped.There are at least three usages of the
ExecutionModel
WMMSolver
: each iteration of the verification will create an execution (in most of the cases inconsistent wrt the memory model) and send this to the theory solver to check for consistency.This use case only requires capturing executed events and base relations.
/home/ponce/git/Dat3M/dartagnan/src/main/java/com/dat3m/dartagnan/witness/grapviz
.We need to allow at least two extra options: show derived relations (given by the user as an option
--witness.doshow=a,b,c
), and show local events (in many cases this will blow up the size of the graph so the option should be off by default)hb
relation in the cat model (file/cat/svcomp.cat
satisfies this). We then create a linearization of the order and convert it to *.graphml format. The current code doing this (but not usingExecutionModel
) is in/home/ponce/git/Dat3M/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml
The text was updated successfully, but these errors were encountered: