Adding Barrier synchronization and Auxiliary Variable examples #177

JarodDif · 2025-07-26T12:53:57Z

This PR contains two specifications created for my Master's thesis that could interest the community.

The specification of the implementation of a barrier and the refinement towards an abstract one.
The usage of auxiliary variables to achieve two-way refinement between Peterson's algorithm and an abstract lock

The specifications have not been added to the CI.

ahelwer · 2025-07-26T17:45:05Z

Thank you for the contributions! Could you please greatly expand both of the READMEs? It should be very clear what each spec is about.

muenchnerkindl

Thanks for these contributions. In particular, the one that constructs a refinement from the two-process lock algorithm to Peterson shows how TLA+ can be used for proving trace equivalence between a high-level and a low-level spec. Although I appreciate your use of TLAPS throughout the developments, I'd suggest to include a few more sanity checks using TLC. Also, morally one assumption should be turned into a theorem (and it is actually true).

Finally, did you try to add your examples to manifest.json and to the top-level README.md? (If you find it too tricky, we can do it for you.)

specifications/barriers/README.md

muenchnerkindl · 2025-07-27T07:14:34Z

specifications/barriers/README.md

+A refinement towards an abstract Barrier specification is proven with TLAPS.
+
+The main invariant `Inv` is verified in the provided model for $N = 7$ 
+processes.


Barriers.tla proves other invariants as well, perhaps they could be included in the configuration? And the proof in Barriers.tla culminates in verifying refinement between the two specifications, TLC could also be used to check this for a finite instance.

muenchnerkindl · 2025-07-27T07:15:06Z

specifications/barriers/README.md

+
+## Barrier.tla
+
+A specification of an abstract Barrier. No model is provided.


Wouldn't it make sense to have TLC check a basic property of that specification as well?

muenchnerkindl · 2025-07-27T07:27:13Z

specifications/locks_auxiliary_vars/LockHS.tla

+VARIABLE s
+INSTANCE Stuttering
+
+ASSUME AltStutterConstantCondition(1..2, 1, LAMBDA j : j-1)


Why is this an assumption? The predicate boils down to
ReachBot[{1}] = 1 .. 2
(with ReachBot defined in the definition of the predicate) and indeed a quick calculation shows that
ReachBot[{1}] = ReachBot[{1,2}] = {1,2}
so the condition holds, so this should really be a theorem. The TLAPS proof of that theorem may be tricky because it involves a recursive function (which, moreover, is defined inside a LET), if you have trouble with it, I can have a try at it.

I could not write a proof for this property, as my knowledge of recursive definitions in TLA+ are lacking.

I would gladly accept some help for this.

muenchnerkindl · 2025-07-27T07:29:44Z

specifications/locks_auxiliary_vars/README.md

+## Peterson.tla
+
+The specification of Peterson's algorithm in PlusCal, and the refinement proof
+towards `Lock!Spec`


This refinement could also be checked using TLC.

muenchnerkindl · 2025-07-27T07:31:38Z

specifications/locks_auxiliary_vars/README.md

+
+The extension of `Lock.tla` using a history variable `h_turn` and a stutter
+variable `s`, provided by the `Stuttering.tla` module. 
+A refinement proof towards `Peterson!Spec` is presented within.


Again, it would make sense to use TLC for checking the different theorems proved in this module?

JarodDif · 2025-07-27T09:45:55Z

I tried to improve the READMEs and the different models.
I'm still unsure if the models I provided to verify refinements are correct / follow best practices.

Concerning manifest.json, the sheer size of the manifest-schema makes me reticent to try and modify it myself.

muenchnerkindl

Thanks for your changes in reply to my previous comments! I added a few final suggestions: some possible additional explanations and perhaps remove the "MC..." module (and integrate the checks into the corresponding base models) whose purpose is not clear to me. It's really up to you if you want to take up these suggestions or not.

muenchnerkindl · 2025-07-30T07:31:00Z

specifications/barriers/MCBarriers.tla

@@ -0,0 +1,6 @@
+------------------------------- MODULE MCBarriers ------------------------------


Why do you really need this module? Usually "MC..." modules are introduced for specializing definitions or introducing additional bounds for model checking, but this is not done here. It looks like you could just add the definition to Barriers.tla and the property to Barriers.cfg?

muenchnerkindl · 2025-07-30T07:34:00Z

specifications/barriers/Barriers.tla

+
+(**
+--algorithm Barrier {
+    variables


It would help the reader if you could add comments describing the purpose of these variables and the basic structure of the algorithm.

muenchnerkindl · 2025-07-30T07:41:15Z

specifications/barriers/Barrier.tla

+
+TypeOK ==
+  /\ pc \in [ProcSet -> {"b0", "b1"}]
+


Perhaps it would make sense to add the property
[][\A p,q \in ProcSet : pc[p] = "b0" /\ pc[q] = "b1" => pc'[q] = "b1"]_vars
that describes the idea of the barrier?

muenchnerkindl · 2025-07-30T07:42:18Z

specifications/barriers/README.md

+A model `MCBarriers.cfg` and its companion `MCBarriers.tla` verifies if
+`B!Spec` (the abstract Barrier specification) holds for `Spec` 
+
+## Barrier.tla


I think it would make sense to talk about Barrier.tla before Barriers.tla – in particular since you mention it in the "Refinement" section.

muenchnerkindl · 2025-07-30T07:42:43Z

specifications/barriers/README.md

+
+The usual typing invariant is defined.
+
+A model with the same amount of processes as above is provided. 


amount -> number (counted, not weighed)

muenchnerkindl · 2025-07-30T07:44:54Z

specifications/locks_auxiliary_vars/MCLockHS.tla

@@ -0,0 +1,7 @@
+------------------------------- MODULE MCLockHS -------------------------------


Again, I wonder why you choose to introduce a separate module for this, given that you already use the model checker on the base LockHS module.

muenchnerkindl · 2025-07-30T07:45:37Z

specifications/locks_auxiliary_vars/MCPeterson.tla

@@ -0,0 +1,6 @@
+------------------------------ MODULE MCPeterson ------------------------------


Same question here: I'd remove this module and include the check in the base Peterson.cfg model.

muenchnerkindl · 2025-07-30T07:48:50Z

specifications/locks_auxiliary_vars/LockHS.tla

+VARIABLE s
+INSTANCE Stuttering
+
+THEOREM StutterConstantCondition(1..2, 1, LAMBDA j : j-1)


Perhaps add a comment saying that this theorem justifies the introduction of s as a stuttering variable in action l1HS below?

muenchnerkindl

LGTM, thanks!

README.md

specifications/barriers/README.md

specifications/locks_auxiliary_vars/README.md

ahelwer · 2025-07-31T16:13:38Z

This repository requires DCO signoff on all commits.

ahelwer · 2025-07-31T16:53:01Z

I opened PR JarodDif#1 which should add these specs to CI validation.

ahelwer · 2025-07-31T17:19:44Z

Some issues with past model names being fixed in #179. @JarodDif would you be able to remove the PR changes I sent you then force-push to this branch to avoid merge conflicts?

ahelwer · 2025-07-31T17:32:23Z

To avoid other weird merge conflicts it's fine to merge this with .ciignore entries in place then I'll add the specs to CI validation later. The specs will have to be removed from the README table for now.

JarodDif · 2025-07-31T17:45:18Z

Would this suffice ?

ahelwer · 2025-07-31T17:54:54Z

Yes, the CI will probably now pass. You still need to add DCO signoff to all your commits (see instructions provided by github here: https://github.com/tlaplus/Examples/pull/177/checks?check_run_id=47140681764) and expand the READMEs.

Signed-off-by: JarodDif <[email protected]>

Co-authored-by: Stephan Merz <[email protected]> Signed-off-by: JarodDif <[email protected]>

Signed-off-by: JarodDif <[email protected]>

Adding descriptions Signed-off-by: JarodDif <[email protected]>

Signed-off-by: JarodDif <[email protected]>

specifications/barriers/README.md

ahelwer · 2025-08-06T15:46:35Z

Looks good! Just clear up that sentence fragment in the barriers README and I will merge.

Signed-off-by: JarodDif <[email protected]>

JarodDif · 2025-08-06T16:01:14Z

This should fix the incomplete sentence.

Thank you for your time and help.

ahelwer · 2025-08-07T19:06:14Z

Thank you for the wonderful examples!

Specs were added in tlaplus#177 Signed-off-by: Andrew Helwer <[email protected]>

Specs were added in #177 Signed-off-by: Andrew Helwer <[email protected]>

muenchnerkindl reviewed Jul 27, 2025

View reviewed changes

muenchnerkindl reviewed Jul 30, 2025

View reviewed changes

muenchnerkindl approved these changes Jul 30, 2025

View reviewed changes

ahelwer reviewed Jul 31, 2025

View reviewed changes

README.md Outdated Show resolved Hide resolved

ahelwer reviewed Jul 31, 2025

View reviewed changes

specifications/barriers/README.md Show resolved Hide resolved

ahelwer reviewed Jul 31, 2025

View reviewed changes

specifications/locks_auxiliary_vars/README.md Show resolved Hide resolved

ahelwer mentioned this pull request Jul 31, 2025

Added barrier and Peterson's refinement models to CI validation JarodDif/Examples#1

Merged

JarodDif force-pushed the master branch from a6487a5 to 3555c05 Compare July 31, 2025 17:29

JarodDif added 10 commits July 31, 2025 19:57

Adding specifications

65f9c06

Signed-off-by: JarodDif <[email protected]>

More verbose Barriers README, better models for invariants

eb93985

Signed-off-by: JarodDif <[email protected]>

Verifying (?) the refinement on a finite model

9852d32

Signed-off-by: JarodDif <[email protected]>

More verbose README for locks, better models, verifying (?) refinements

8dfe57d

Signed-off-by: JarodDif <[email protected]>

Adding specifications to the top-level README

16d33d3

Signed-off-by: JarodDif <[email protected]>

Adding proof for StutterConstantCondition

684667d

Co-authored-by: Stephan Merz <[email protected]> Signed-off-by: JarodDif <[email protected]>

Unify TLC models for locks_auxiliary_vars

7fb278e

Signed-off-by: JarodDif <[email protected]>

Unify TLC models for barriers

d7a0bde

Adding descriptions Signed-off-by: JarodDif <[email protected]>

Adding more details in READMEs

390f712

Signed-off-by: JarodDif <[email protected]>

Remove Specs from README for CI

4174402

Signed-off-by: JarodDif <[email protected]>

JarodDif force-pushed the master branch from 5df18a1 to 4174402 Compare July 31, 2025 17:57

Added link to master's thesis and misc. additions

4fabe41

Signed-off-by: JarodDif <[email protected]>

ahelwer reviewed Aug 6, 2025

View reviewed changes

specifications/barriers/README.md Outdated Show resolved Hide resolved

Finished incomplete paragraph

1e56456

Signed-off-by: JarodDif <[email protected]>

ahelwer merged commit 11c7cd8 into tlaplus:master Aug 7, 2025
7 checks passed

ahelwer added a commit to ahelwer/Examples that referenced this pull request Aug 8, 2025

Added barrier and peterson's algorithm specs to CI

26d45e8

Specs were added in tlaplus#177 Signed-off-by: Andrew Helwer <[email protected]>

ahelwer mentioned this pull request Aug 8, 2025

Added barrier and peterson's algorithm specs to CI #183

Merged

ahelwer added a commit to ahelwer/Examples that referenced this pull request Aug 8, 2025

Added barrier and peterson's algorithm specs to CI

8873140

Specs were added in tlaplus#177 Signed-off-by: Andrew Helwer <[email protected]>

ahelwer added a commit to ahelwer/Examples that referenced this pull request Aug 8, 2025

Added barrier and peterson's algorithm specs to CI

53a6b74

Specs were added in tlaplus#177 Signed-off-by: Andrew Helwer <[email protected]>

ahelwer added a commit that referenced this pull request Aug 8, 2025

Added barrier and peterson's algorithm specs to CI

18c5810

Specs were added in #177 Signed-off-by: Andrew Helwer <[email protected]>


		## Barrier.tla

		A specification of an abstract Barrier. No model is provided. No newline at end of file

		@@ -0,0 +1,6 @@
		------------------------------- MODULE MCBarriers ------------------------------


		The usual typing invariant is defined.

		A model with the same amount of processes as above is provided. No newline at end of file

		@@ -0,0 +1,7 @@
		------------------------------- MODULE MCLockHS -------------------------------

		@@ -0,0 +1,6 @@
		------------------------------ MODULE MCPeterson ------------------------------

Adding Barrier synchronization and Auxiliary Variable examples #177

Adding Barrier synchronization and Auxiliary Variable examples #177

Uh oh!

Conversation

JarodDif commented Jul 26, 2025

Uh oh!

ahelwer commented Jul 26, 2025

Uh oh!

muenchnerkindl left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

JarodDif commented Jul 27, 2025

Uh oh!

muenchnerkindl left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

muenchnerkindl left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ahelwer commented Jul 31, 2025

Uh oh!

ahelwer commented Jul 31, 2025

Uh oh!

ahelwer commented Jul 31, 2025

Uh oh!

ahelwer commented Jul 31, 2025

Uh oh!

JarodDif commented Jul 31, 2025

Uh oh!

ahelwer commented Jul 31, 2025

Uh oh!

Uh oh!

ahelwer commented Aug 6, 2025

Uh oh!

JarodDif commented Aug 6, 2025

Uh oh!

Uh oh!

ahelwer commented Aug 7, 2025

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

4 participants