From d48fbebd9fb643a6a014e389ab4e72a0d40e0edb Mon Sep 17 00:00:00 2001 From: Luca BRUNO Date: Wed, 4 Sep 2024 10:04:04 +0200 Subject: [PATCH 1/2] examples: add Lamport's concurrency teaching algorithm This adds a simple concurrent algorithm described by Lamport in https://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf. It provides an arbitrary-N module and a concrete-N instance. It shows how to use temporal formulas and check for (eventual and correct) termination in the verifier. --- examples/.scripts/run-example.sh | 2 + examples/README.md | 1 + .../teachingConcurrency.qnt | 101 ++++++++++++++++++ 3 files changed, 104 insertions(+) create mode 100644 examples/classic/distributed/TeachingConcurrency/teachingConcurrency.qnt diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh index e8f7753e8..b1de4db9b 100755 --- a/examples/.scripts/run-example.sh +++ b/examples/.scripts/run-example.sh @@ -136,6 +136,8 @@ get_verify_args () { args="--init=Init --step=Next" elif [[ "$file" == "games/tictactoe/tictactoe.qnt" ]] ; then args="--max-steps=1" # pretty slow, and we just want to check that verification can run + elif [[ "$file" == "classic/distributed/TeachingConcurrency/teachingConcurrency.qnt" ]] ; then + args="--temporal correct" fi echo "${args}" } diff --git a/examples/README.md b/examples/README.md index 183b6df69..97f3e36d7 100644 --- a/examples/README.md +++ b/examples/README.md @@ -54,6 +54,7 @@ listed without any additional command line arguments. | [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1284 | | [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] | | [classic/distributed/ReadersWriters/ReadersWriters.qnt](./classic/distributed/ReadersWriters/ReadersWriters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | +| [classic/distributed/TeachingConcurrency/teachingConcurrency.qnt](./classic/distributed/TeachingConcurrency/teachingConcurrency.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | | [classic/distributed/TwoPhaseCommit/two_phase_commit.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | | [classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt) | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/1299 | :x:https://github.com/informalsystems/quint/issues/1299 | | [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | diff --git a/examples/classic/distributed/TeachingConcurrency/teachingConcurrency.qnt b/examples/classic/distributed/TeachingConcurrency/teachingConcurrency.qnt new file mode 100644 index 000000000..f043c8bb6 --- /dev/null +++ b/examples/classic/distributed/TeachingConcurrency/teachingConcurrency.qnt @@ -0,0 +1,101 @@ +// -*- mode: Bluespec; -*- +/** + * A simple algorithm from Lamport's "Teaching Concurrency" paper: + * https://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf + * + * Run in verifier with: + * quint verify --temporal correct teachingConcurrency.qnt + */ + +// An example instance of the algorithm with N=5. +module teachingConcurrency { + import teachingConcurrencyN(NUM_PROCS=5).* +} + +// A concurrency algorithm providing a basic form of mutual +// exclusion. For details and proofs see section 7.2 of +// https://lamport.azurewebsites.net/tla/proving-safety.pdf +module teachingConcurrencyN { + // N processes (numbered from 0 to N-1). + const NUM_PROCS: int + assume nonEmpty = NUM_PROCS >= 1 + + var x: List[int] + var y: List[int] + + // Set of processes yet to be executed. + var pendingProcs: Set[int] + + // Initial state: + // - x and y zeroed for all processes + // - all processes pending scheduling + action init = all { + x' = zeroes(NUM_PROCS), + y' = zeroes(NUM_PROCS), + pendingProcs' = 0.to(NUM_PROCS-1), + } + + // Stepping action: randomly pick a pending process (if + // any) and execute it. Otherwise stutter forever, as + // every process has stopped. + action step = any { + all { + not(termination), + processUpdate, + }, + all { + termination, + allStopped, + } + } + + // Execute the algorithm for a pending process. + action processUpdate = { + nondet proc = pendingProcs.oneOf() + + val nextX = x.replaceAt(proc, 1) + val index = circularIndex(proc, NUM_PROCS) + val yValue = nextX[index] + + all { + x' = nextX, + y' = y.replaceAt(proc, yValue), + pendingProcs' = pendingProcs.exclude(Set(proc)), + } + } + + // All processes have stopped. + action allStopped = all { + x' = x, + y' = y, + pendingProcs' = pendingProcs, + } + + // Return a List of 0s, with the given length. + pure def zeroes(len: int): List[int] = { + 0.to(len-1).fold(List(), (l, _) => l.append(0)) + } + + // Calculate the circular index `(i-1) mod N`. + pure def circularIndex(i: int, N: int): int = { + if (i == 0) { + N-1 + } else { + i-1 + } + } + + // Correctness invariant: (after every process has + // stopped) y[i] == 1 for at least one process. + val yContainsOne = { + y.select(v => v == 1).length() >= 1 + } + + // Termination invariant: all processes have stopped + // (i.e. none is pending scheduling). + val termination = { + pendingProcs.size() == 0 + } + + temporal correct = eventually(termination and yContainsOne) +} From c78e6814394ad7a30aa9de307ac3d7d471106a85 Mon Sep 17 00:00:00 2001 From: Luca Bruno Date: Wed, 4 Sep 2024 15:34:01 +0200 Subject: [PATCH 2/2] examples: cleanup teachingConcurrency Co-authored-by: Gabriela Moreira --- .../TeachingConcurrency/teachingConcurrency.qnt | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/examples/classic/distributed/TeachingConcurrency/teachingConcurrency.qnt b/examples/classic/distributed/TeachingConcurrency/teachingConcurrency.qnt index f043c8bb6..6de668fcd 100644 --- a/examples/classic/distributed/TeachingConcurrency/teachingConcurrency.qnt +++ b/examples/classic/distributed/TeachingConcurrency/teachingConcurrency.qnt @@ -38,14 +38,11 @@ module teachingConcurrencyN { // Stepping action: randomly pick a pending process (if // any) and execute it. Otherwise stutter forever, as // every process has stopped. - action step = any { - all { - not(termination), - processUpdate, - }, - all { - termination, - allStopped, + action step = { + if (termination) { + allStopped + } else { + processUpdate } }