search

Gabriella439 / HasCal

Haskell embedding of PlusCal
BSD 3-Clause "New" or "Revised" License
61 stars 6 forks source link

Checking mutual exclusion for FastMutex #1

Closed stevana closed 2 years ago

stevana commented 2 years ago

I suppose we would like to do something like this:

            yield CriticalSection
+           assert (forall_ [ 1 .. n ] \i ->
+                      i /= self ==> pc i /= CriticalSection)
            yield (Line 11)

But I don't see how it would be possible to implement pc given the current definition of Process (because the current process doesn't know the label other processes are at).

I guess we could add _pcs :: HashMap Int Label to FastMutex's Global state and update it on every yield, but there ought to be a better way? Thoughts?

Gabriella439 commented 2 years ago

Yeah, I hadn't gotten to that because I'm still implementing support for temporal expressions and model checking invariants but you're right that the state would need to be moved to the Global state as a HashMap, similar to the original example from the PlusCal manual

Gabriella439 commented 2 years ago

Alright, this is fixed now that I've added support for model checking invariants. You can find the equivalent property here:

https://github.com/Gabriel439/HasCal/blob/e095e70ef45c80c1bd4a53768d7c09687a5d4b60/tasty/HasCal/Test/FastMutex.hs#L47-L50