Re: [tlaplus] Checking invariants periods during periods of quiescence

\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.

On 1 Sep 2020, at 06:44, Jedd Haberstro <jhaberstro@xxxxxxxxx> wrote:

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.
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.
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!

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/cbe356b5-8e04-44b0-a0fd-141d2a565ca7n%40googlegroups.com.