CinRC / IRDC-CCSK

Java implementation of distributed reversible computation verification
https://spots.augusta.edu/caubert/cinrc/
GNU General Public License v3.0
4 stars 2 forks source link

Toward equivalences #21

Closed aubertc closed 1 year ago

aubertc commented 2 years ago

The goal of this issue is to start implementing equivalences between processes. We could start with an "easy" trace equivalence:

image

So, for instance, you would have tr(a.b + (c|d)) = {ab, cd, dc}
and tr(a.b + c.d + d.c.) = tr(a.b + (c|d))

(Things get a bit more complicated with synchronizations, but we can worry about that later)

A possible way to obtain this first type of equivalence would be to:

Later on, we could try to have more "subtle" equivalences, that would require e.g. to have a way of acknowledging that (a[k1] | b[k2]) and (a[k2] | b[k1]) are actually the same process (note that this is not widely accepted in the reversible community, so we may want to be careful with that)

aubertc commented 1 year ago

I don't think we need any of that since https://github.com/CinRC/IRDC-CCSK/pull/64, as we now have actual equivalences implemented.