search

emichael / dslabs

Distributed Systems Labs and Framework
https://ellismichael.com/dslabs/
1.26k stars 341 forks source link

Feature Request: add detail messages for more/all invariant predicates #34

Closed gnanabite closed 2 years ago

gnanabite commented 2 years ago

Currently, some invariant predicates do not have detail messages. The most prominent one is the APPENDS_LINEARIZABLE predicate. It could be useful to explain why the invariant was violated (e.g., for APPENDS_LINEARIZABLE, we could write something like "AppendResult(y) is not a valid result for Append(x)", or "AppendResult(y) for client 2 is inconsistent with AppendResult(x) for client 1"). The other invariant I see is MULTI_GETS_MATCH.

These omissions might be intentional (e.g., maybe the goal is to get students to identify what's wrong in the sequence), so I'm not opening a pull request yet.

emichael commented 2 years ago

100% just an oversight; something I meant to do but never got around to. I don't think there's any reason not to display a message. If you want to open up a PR, go for it!

emichael commented 2 years ago

Leaving open since there's still MULTI_GETS_MATCH.