Checking invariants periods during periods of quiescence

[Jedd Haberstro]

Hi all,

I am modeling a concurrent data structure in PlusCal. There are invariants that may become false during method invocations, but which should become true once all such invocations have completed (during periods of "quiescence", if you will).

Is there a customary way to model check such types of invariants? Two approaches immediately come to mind, but I don't know if better approaches exist.

1. Check the invariant only when all processes' pc variables are equal to a label contained from within the relevant invocations' implementation. e.g. (\A p \in ProcSet : ~(pc[p] \in InvocationLabels)) => QuiescenceInvariant. This is quite a hairy approach because it will be error prone keeping InvocationLabels in sync with the PlusCal code.
2. A liveness property that states that if QuiescenceInvariant is not true, then it will eventually become true. e.g. ~QuiescenceInvariant ~> QuiescenceInvariant. However, this seems too imprecise because I believe it will be trivially satisfied when the algorithm terminates. I could probably add more constraints on this, but I imagine those constraints will just introduce new issues that need new constraints.

Any better ideas? :-)

Thanks,

Jedd

P.S. It's been ~2-3 weeks since I started learning TLA+/PlusCal and already I feel very productive! Kudos to the community for creating such a wonderfully approachable tool. The syntax is simple and readable, the toolbox is proving to be a helpful development environment, and the freely available learning material (e.g. Leslie's books and video course) is top notch. So, thank you all!

[Stephan Merz]

Hi,

the first approach that you describe is the standard way to check that a predicate holds throughout the execution except at certain control points. TLC will help you maintain an appropriate definition of the set of exceptions.

Your second suggestion is complementary: it ensures that the predicates are eventually restored [1]. If you've already checked the first property you can also write

\A p \in ProcSet : []<> ~(pc[p] \notin InvocationLabels)

or perhaps even

\A p \in ProcSet : <>[] ~(pc[p] \notin InvocationLabels)

if violations of the predicate are not recurrent.

Best,

Stephan

[1] Remember that a safety property is true of an algorithm that does nothing. In particular, checking your invariant won't require any fairness assumption, but the liveness property will.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/cbe356b5-8e04-44b0-a0fd-141d2a565ca7n%40googlegroups.com.

[Jedd Haberstro]

Hi Stephan,

Thank you for your guidance.

I already check that my system terminates, so I believe the extra reassurance that the predicates are eventually restored is not useful since, when terminated, \A p \in ProcSet : (pc[p] \notin InvocationLabels) will also hold.

Thanks,

Jedd