Release/Acquire consistency

[volodeyka]

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. Where wb defined as follows:

So as I see our plan is:

• Define RA-consistency predicate in terms of ca-relation. To do this I propose to define wb-function of E -> seq E type using strict ca version. Then we can ask something like x \notin wb x for all x from dom es
• Make a new function eval_RA_step that takes RA-consistent configuration c and returns sequence of all RA-consistent configurations that we can rich from c by one step i.e. we should filter all possible configurations by RA-consistency predicate
• We should proof that if there is wb-cycle in some event structure es then there is `wb-cycle in it's conflict free subset.
• I guess that if we know that es is RA-consistent, then there is a simpler way to ensure that add_event x es is RA-consistent then just check RA-consistency predicate. So it would be great to come up with such predicate
• Finally, we should proof that if es is RA-consistent, than exists such mo relation that is acyclic

[eupp]

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.

[volodeyka]

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

[eupp]

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

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 fsfuns, and the second one builds the proofs, assuming some preconditions hold.