[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Checking invariants periods during periods of quiescence

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!

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