Open volodeyka opened 3 years ago
I think it would be good to split this into two subtasks. 1) Filtration of the event structures by the consistency predicate. 2) Definition and properties of RA-consistency.
For example, I don't think we need a separate eval_RA_step
(or, in general, a new eval_MM_step
for each imaginable memory model). Instead, I think, we should define a small-step function that just filters out inconsistent event structures (using some consistency predicate). Then, depending on particular properties of the consistency predicate, we can develop more specialized/efficient versions of the small-step function, which, for example, would not just check the consistency naively, but would filter-out some inconsistent reads-from options.
So for example, currently we have what you called ces_seq
, which filters out some reads-from options, that would otherwise lead to a violation of hereditary property e1 <= e2 -> e2 # e3 -> e1 # e3
. So why not try to generalize it, by abstracting over the consistency predicate? In essence, the idea is the same for all memory models, you just try to add a new event to an event structure, and then filter out some inconsistent event structures.
So why not try to generalize it, by abstracting over the consistency predicate?
Shouldn't we add some memory-model filtration after ces_seq
? Because without it we can't obtain prime event structure form exec_eventstructure
, and this violate our "event-structure"-ideology
So why not try to generalize it, by abstracting over the consistency predicate?
Shouldn't we add some memory-model filtration after
ces_seq
? Because without it we can't obtain prime event structure formexec_eventstructure
, and this violate our "event-structure"-ideology
Would be nice to unify the two.
We can split the fin_exec_event_struct
into two subparts, one is data
and the second one is data+proofs
.
Then we'll have two functions, the first one just updates the data
part by updating underlying fsfun
s, and the second one builds the proofs, assuming some preconditions hold.
After pushing #73, we'll be finally ready to reason about R/A consistency. Here I want to make some kind of plan. We know that execution graph is RA consistent iff
wb
-relation is acyclic. Wherewb
defined as follows:So as I see our plan is:
ca
-relation. To do this I propose to definewb
-function ofE -> seq E
type using strictca
version. Then we can ask something likex \notin wb x
for all x fromdom es
eval_RA_step
that takes RA-consistent configurationc
and returns sequence of all RA-consistent configurations that we can rich fromc
by one step i.e. we should filter all possible configurations by RA-consistency predicatewb
-cycle in some event structurees
then there is `wb-cycle in it's conflict free subset.es
is RA-consistent, then there is a simpler way to ensure thatadd_event x es
is RA-consistent then just check RA-consistency predicate. So it would be great to come up with such predicatees
is RA-consistent, than exists suchmo
relation that is acyclic