From 647af0011f8d3c3ac9101d4b34a6da33b8b6fc3b Mon Sep 17 00:00:00 2001 From: kirdatatjana Date: Thu, 7 Nov 2024 18:04:21 +0100 Subject: [PATCH 1/4] Added quint example for Algorithm 15 --- .../ConsensusAlgorithm/ConsensusAlg.qnt | 255 ++++++++++++++++++ 1 file changed, 255 insertions(+) create mode 100644 examples/classic/distributed/ConsensusAlgorithm/ConsensusAlg.qnt diff --git a/examples/classic/distributed/ConsensusAlgorithm/ConsensusAlg.qnt b/examples/classic/distributed/ConsensusAlgorithm/ConsensusAlg.qnt new file mode 100644 index 000000000..5ec88b227 --- /dev/null +++ b/examples/classic/distributed/ConsensusAlgorithm/ConsensusAlg.qnt @@ -0,0 +1,255 @@ +// -*- mode: Bluespec; -*- + + /************************************************************************************************ + (* Quint Specification for Algorithm 15: Consensus Algorithm in the Presence of Crash Failures *) + (* This specification is derived from book "Distributed Computing: Fundamentals, Simulations, *) + (* and Advanced Topics" (Second Edition) by Hagit Attiya and Jennifer Welch, specifically from *) + (* Chapter 5, page 93. *) + (* http://lib.ysu.am/disciplines_bk/c95d04e111f3e28ae4cc589bfda1e18b.pdf *) + ************************************************************************************************/ +module ConsensusAlg { + + const N : int + const F : int + const actualFaults : int + + type Proc = int + type Value = int + type Round = int + type Message = { sender: Proc, values: Set[Value] } + + type Decision = + | None + | Some(Value) + + type LocalState = { + V: Set[Value], + k: Round, + y: Decision, + S: Set[Set[Value]], + x: Value + } + + // + // Local functions + // + + def getFirst(s: Set[int]): int = s.fold(0, (_, v) => v) + + def minValue(values: Set[int]): int = { val initial = getFirst(values) values.fold(initial, (min, v) => if (v < min) v else min) } + + pure def compute(s: LocalState): LocalState = { + + val newV = s.V.union(flatten(s.S)) + val newK = s.k + 1 + val newY = if (newK == F + 1) Some(minValue(newV)) else s.y + + { + V: newV, + k: newK, + y: newY, + S: Set(), + x: s.x + } + } + + // + // State machine + // + + val Procs: Set[int] = 1.to(N - 1) + + var round: Round + var correctProcsMessages: Set[Message] + var crashedProcsMessages: Set[Message] + var procState: int -> LocalState + var crashed: Set[int] + var newlyCrashed: Set[int] + + // + // Invariants + // + + def agreement = Procs.exclude(crashed).forall(p => + Procs.exclude(crashed).forall(q => + ( procState.get(p).y != None and procState.get(q).y != None) implies + procState.get(p).y == procState.get(q).y)) + + /// If all processes have the same initial value v, then this must be the only decision value + def validity = + val allXValues = Procs.map(p => procState.get(p).x) + if (allXValues.size() == 1) + allXValues.forall(v => + Procs.exclude(crashed).forall(p => + match procState.get(p).y { + | Some(y) => y == v + | None => true + })) + else + true + + // + // Steps + // + + action init = all { + nondet initialValues = Procs.setOfMaps(Set(1, 2, 3)).oneOf() + procState' = Procs.mapBy(i => { + V: Set(initialValues.get(i)), + k: 1, + y: None, + S: Set(), + x: initialValues.get(i) + }), + round' = 1, + correctProcsMessages' = Set(), + crashed' = Set(), + newlyCrashed' = Set(), + crashedProcsMessages' = Set() + } + + action initializeProcsStateWithDistinctValues = all { + procState' = Procs.mapBy(i => { + V: Set(i), + k: 1, + y: None, + S: Set(), + x: i + }), + round' = 1, + correctProcsMessages' = Set(), + crashed' = Set(), + newlyCrashed' = Set(), + crashedProcsMessages' = Set() + } + + action sendMessages = all { + if (round <= F + 1) + correctProcsMessages' = Procs.exclude(crashed).exclude(newlyCrashed).map(p => { + sender: p, + values: procState.get(p).V + }) + else + correctProcsMessages' = correctProcsMessages, + if(newlyCrashed.size() > 0){ + crashedProcsMessages' = newlyCrashed.map(p => { + sender: p, + values: procState.get(p).V + }) + } else{ + crashedProcsMessages' = crashedProcsMessages + }, + round' = round, + procState' = procState, + crashed' = crashed, + newlyCrashed' = newlyCrashed + } + + action crashProcess(p) = all { + newlyCrashed' = Set(p), + crashed' = crashed, + round' = round, + procState' = procState, + correctProcsMessages' = correctProcsMessages, + crashedProcsMessages' = crashedProcsMessages + } + + action randCrash = all { + if (actualFaults - crashed.size() > 0) { + nondet newCrashCount = oneOf(1.to(actualFaults - crashed.size())) + newlyCrashed' = Procs.exclude(crashed).powerset().filter(s => s.size() == newCrashCount).oneOf() + } else { + newlyCrashed' = newlyCrashed + }, + crashed' = crashed, + round' = round, + procState' = procState, + correctProcsMessages' = correctProcsMessages, + crashedProcsMessages' = crashedProcsMessages + } + + action receiveMessages = all { + round' = round, + correctProcsMessages' = Set(), + crashedProcsMessages' = Set(), + val newCorrectValues: Set[Set[Value]] = correctProcsMessages.map(m => m.values) + if (crashedProcsMessages.size() == 0){ + procState' = procState.keys().mapBy(p => {... procState.get(p), S:newCorrectValues}) + } + else{ + val newCrashedProcsValues: Set[Set[Value]] = crashedProcsMessages.map(m => m.values) + nondet crashedMessagesRecived = Procs.setOfMaps(newCrashedProcsValues).union(Set()).oneOf()// for each process we pick from which newly crashed they receive a message + procState' = procState.keys().mapBy(p => { ... procState.get(p), S: newCorrectValues.union(Set(crashedMessagesRecived.get(p))) }) + }, + crashed' = crashed, + newlyCrashed' = newlyCrashed, + } + + action computeAction = all { + correctProcsMessages' = Set(), + procState' = procState.keys().mapBy(p => compute(procState.get(p))), + round' = round + 1, + crashed' = crashed.union(newlyCrashed), + newlyCrashed' = Set(), + crashedProcsMessages' =Set() + } + + /// the set s of correct processes don't receive the messages from newlycrashed + action receiveMessage(s) = all { + round' = round, + correctProcsMessages' = Set(), + crashedProcsMessages' = Set(), + val newCorrectValues: Set[Set[Value]] = correctProcsMessages.map(m => m.values) + val newCrashedProcsValues: Set[Set[Value]] = crashedProcsMessages.map(m => m.values) + procState' = procState.keys().mapBy(p => + { ...procState.get(p), + S: if (s.contains(p)) + newCorrectValues + else + newCorrectValues.union(newCrashedProcsValues) + } + ), + crashed' = crashed, + newlyCrashed' = newlyCrashed, + } + + action step = any{ + randCrash.then(sendMessages).then(receiveMessages).then(computeAction) + } + + /// we crash process p, and the set s does not receive p's messages + action stepHidePsMessagesFromS(p,s) = any{ + crashProcess(p).then(sendMessages).then(receiveMessage(s)).then(computeAction) + } + +} + +module properValues { + //quint run --main=properValues ConsensusAlg.qnt + import ConsensusAlg(N = 6, F = 1, actualFaults = 1 ).* + + run consensusRunTest = + init + .then((F + 1).reps(_ => step)) + .expect(agreement) + .expect(validity) +} + + +module badValues { + //quint run ConsensusAlg.qnt --main badValues --invariant agreement --max-steps 5 + //quint test --main=badValues ConsensusAlg.qnt + import ConsensusAlg(N = 6, F = 1, actualFaults = 2 ).* + + run consensusRunTest = + init + .then((F + 1).reps(_ => step)) + .expect(validity) + + run consensusDisagreementTest = + initializeProcsStateWithDistinctValues + .then(stepHidePsMessagesFromS(1, Set(2))) + .then(stepHidePsMessagesFromS(3, Set(4))) + .expect(not(agreement)) + +} From 66da17154f660b5890637225556f2c7e1021580a Mon Sep 17 00:00:00 2001 From: kirdatatjana Date: Thu, 7 Nov 2024 18:09:53 +0100 Subject: [PATCH 2/4] Added initial implementation of Algorithm 18 --- .../KSetAgreementConsensus.qnt | 264 ++++++++++++++++++ 1 file changed, 264 insertions(+) create mode 100644 examples/classic/distributed/ConsensusAlgorithm/KSetAgreementConsensus.qnt diff --git a/examples/classic/distributed/ConsensusAlgorithm/KSetAgreementConsensus.qnt b/examples/classic/distributed/ConsensusAlgorithm/KSetAgreementConsensus.qnt new file mode 100644 index 000000000..65ac6f322 --- /dev/null +++ b/examples/classic/distributed/ConsensusAlgorithm/KSetAgreementConsensus.qnt @@ -0,0 +1,264 @@ +// -*- mode: Bluespec; -*- + + /****************************************************************************************************** + (* Quint Specification for Algorithm 18: K-set Consensus Algorithm in the Presence of Crash Failures *) + (* This specification is derived from book "Distributed Computing: Fundamentals, Simulations, and *) + (* Advanced Topics" (Second Edition) by Hagit Attiya and Jennifer Welch, specifically from Chapter 5, *) + (* page 120. *) + (* http://lib.ysu.am/disciplines_bk/c95d04e111f3e28ae4cc589bfda1e18b.pdf *) + *******************************************************************************************************/ +module KSetAgreementConsensus { + + const N : int + const F : int + const actualFaults : int + const K : int + + type Proc = int + type Value = int + type Round = int + type Message = { sender: Proc, values: Set[Value] } + + type Decision = + | None + | Some(Value) + + type LocalState = { + V: Set[Value], + r: Round, + y: Decision, + S: Set[Set[Value]], + x: Value + } + + // + // Local functions + // + + def getFirst(s: Set[int]): int = s.fold(0, (_, v) => v) + + def minValue(values: Set[int]): int = { val initial = getFirst(values) values.fold(initial, (min, v) => if (v < min) v else min) } + + pure def compute(s: LocalState): LocalState = { + + val newV = s.V.union(flatten(s.S)) + val newK = s.r + 1 + val newY = if (newK == F/K + 1) Some(minValue(newV)) else s.y + + { + V: newV, + r: newK, + y: newY, + S: Set(), + x: s.x + } + } + + // + // State machine + // + + val Procs: Set[int] = 1.to(N - 1) + + var round: Round + var correctProcsMessages: Set[Message] + var crashedProcsMessages: Set[Message] + var procState: int -> LocalState + var crashed: Set[int] + var newlyCrashed: Set[int] + + // + // Invariants + // + + def agreement = Procs.exclude(crashed).forall(p => + Procs.exclude(crashed).forall(q => + ( procState.get(p).y != None and procState.get(q).y != None) implies + procState.get(p).y == procState.get(q).y)) + + def kSetAgreement = { + // Get all decided values (excluding None) and ensure they are unique + val decidedValues = Procs.exclude(crashed).map(p => procState.get(p).y).filter(v => v != None) + + // Check that number of unique decided values is at most K + decidedValues.size() <= K + } + /// If all processes have the same initial value v, then this must be the only decision value + def validity = + val allXValues = Procs.map(p => procState.get(p).x) + if (allXValues.size() == 1) + allXValues.forall(v => + Procs.exclude(crashed).forall(p => + match procState.get(p).y { + | Some(y) => y == v + | None => true + })) + else + true + + // + // Steps + // + + action init = all { + nondet initialValues = Procs.setOfMaps(Set(1, 2, 3)).oneOf() + procState' = Procs.mapBy(i => { + V: Set(initialValues.get(i)), + r: 1, + y: None, + S: Set(), + x: initialValues.get(i) + }), + round' = 1, + correctProcsMessages' = Set(), + crashed' = Set(), + newlyCrashed' = Set(), + crashedProcsMessages' = Set() + } + + action initializeProcsStateWithDistinctValues = all { + procState' = Procs.mapBy(i => { + V: Set(i), + r: 1, + y: None, + S: Set(), + x: i + }), + round' = 1, + correctProcsMessages' = Set(), + crashed' = Set(), + newlyCrashed' = Set(), + crashedProcsMessages' = Set() + } + + action sendMessages = all { + if (round <= F/K + 1) + correctProcsMessages' = Procs.exclude(crashed).exclude(newlyCrashed).map(p => { + sender: p, + values: procState.get(p).V + }) + else + correctProcsMessages' = correctProcsMessages, + if(newlyCrashed.size() > 0){ + crashedProcsMessages' = newlyCrashed.map(p => { + sender: p, + values: procState.get(p).V + }) + } else{ + crashedProcsMessages' = crashedProcsMessages + }, + round' = round, + procState' = procState, + crashed' = crashed, + newlyCrashed' = newlyCrashed + } + + action crashProcess(p) = all { + newlyCrashed' = Set(p), + crashed' = crashed, + round' = round, + procState' = procState, + correctProcsMessages' = correctProcsMessages, + crashedProcsMessages' = crashedProcsMessages + } + + action randCrash = all { + if (actualFaults - crashed.size() > 0) { + nondet newCrashCount = oneOf(1.to(actualFaults - crashed.size())) + newlyCrashed' = Procs.exclude(crashed).powerset().filter(s => s.size() == newCrashCount).oneOf() + } else { + newlyCrashed' = newlyCrashed + }, + crashed' = crashed, + round' = round, + procState' = procState, + correctProcsMessages' = correctProcsMessages, + crashedProcsMessages' = crashedProcsMessages + } + + action receiveMessages = all { + round' = round, + correctProcsMessages' = Set(), + crashedProcsMessages' = Set(), + val newCorrectValues: Set[Set[Value]] = correctProcsMessages.map(m => m.values) + if (crashedProcsMessages.size() == 0){ + procState' = procState.keys().mapBy(p => {... procState.get(p), S:newCorrectValues}) + } + else{ + val newCrashedProcsValues: Set[Set[Value]] = crashedProcsMessages.map(m => m.values) + nondet crashedMessagesRecived = Procs.setOfMaps(newCrashedProcsValues).union(Set()).oneOf()// for each process we pick from which newly crashed they receive a message + procState' = procState.keys().mapBy(p => { ... procState.get(p), S: newCorrectValues.union(Set(crashedMessagesRecived.get(p))) }) + }, + crashed' = crashed, + newlyCrashed' = newlyCrashed, + } + + action computeAction = all { + correctProcsMessages' = Set(), + procState' = procState.keys().mapBy(p => compute(procState.get(p))), + round' = round + 1, + crashed' = crashed.union(newlyCrashed), + newlyCrashed' = Set(), + crashedProcsMessages' =Set() + } + + /// the set s of correct processes don't receive the messages from newlycrashed + action receiveMessage(s) = all { + round' = round, + correctProcsMessages' = Set(), + crashedProcsMessages' = Set(), + val newCorrectValues: Set[Set[Value]] = correctProcsMessages.map(m => m.values) + val newCrashedProcsValues: Set[Set[Value]] = crashedProcsMessages.map(m => m.values) + procState' = procState.keys().mapBy(p => + { ...procState.get(p), + S: if (s.contains(p)) + newCorrectValues + else + newCorrectValues.union(newCrashedProcsValues) + } + ), + crashed' = crashed, + newlyCrashed' = newlyCrashed, + } + + action step = any{ + randCrash.then(sendMessages).then(receiveMessages).then(computeAction) + } + + /// we crash process p, and the set s does not receive p's messages + action stepHidePsMessagesFromS(p,s) = any{ + crashProcess(p).then(sendMessages).then(receiveMessage(s)).then(computeAction) + } + +} + +module properValues { + //quint run --main=properValues KSetAgreementConsensus.qnt + import KSetAgreementConsensus(N = 6, F = 4, actualFaults = 2, K = 2 ).* + + run consensusRunTest = + init + .then((F/K + 1).reps(_ => step)) + .expect(kSetAgreement) + .expect(validity) +} + + +module badValues { + //quint run KSetAgreementConsensus.qnt --main badValues --invariant kSetAgreement --max-steps 5 + //quint test --main=badValues KSetAgreementConsensus.qnt + import KSetAgreementConsensus(N = 8, F = 4, actualFaults = 5, K = 2 ).* + + run consensusRunTest = + init + .then((F/K + 1).reps(_ => step)) + .expect(validity) + + run consensusDisagreementTest = + initializeProcsStateWithDistinctValues + .then(stepHidePsMessagesFromS(1, Set(2,4))) + .then(stepHidePsMessagesFromS(3, Set(4))) + .then(stepHidePsMessagesFromS(5, Set(6))) + .expect(not(kSetAgreement)) + +} From 848cbaa869046f4ae9297860af92c153eed31481 Mon Sep 17 00:00:00 2001 From: Tatjana Date: Wed, 13 Nov 2024 23:48:49 +0100 Subject: [PATCH 3/4] Added receiveMessagesWithHiding --- .../KSetAgreementConsensus.qnt | 74 ++++++++++++++++--- 1 file changed, 65 insertions(+), 9 deletions(-) diff --git a/examples/classic/distributed/ConsensusAlgorithm/KSetAgreementConsensus.qnt b/examples/classic/distributed/ConsensusAlgorithm/KSetAgreementConsensus.qnt index 65ac6f322..1c06d4968 100644 --- a/examples/classic/distributed/ConsensusAlgorithm/KSetAgreementConsensus.qnt +++ b/examples/classic/distributed/ConsensusAlgorithm/KSetAgreementConsensus.qnt @@ -31,6 +31,11 @@ module KSetAgreementConsensus { x: Value } + type HiddenProcs = { + hiddenProcs: Set[Proc], // processes whose messages are hidden + targetProc: Proc // process from which messages are hidden + } + // // Local functions // @@ -176,6 +181,16 @@ module KSetAgreementConsensus { crashedProcsMessages' = crashedProcsMessages } + action crashProcessesFromConfig(hidingConfigs) = all { + // Collect all processes that need to be crashed from all hiding configurations + newlyCrashed' = flatten(hidingConfigs.map(config => config.hiddenProcs)), + crashed' = crashed, + round' = round, + procState' = procState, + correctProcsMessages' = correctProcsMessages, + crashedProcsMessages' = crashedProcsMessages + } + action receiveMessages = all { round' = round, correctProcsMessages' = Set(), @@ -221,20 +236,53 @@ module KSetAgreementConsensus { newlyCrashed' = newlyCrashed, } + action receiveMessagesWithHiding(hidingConfigs) = all { + round' = round, + correctProcsMessages' = Set(), + crashedProcsMessages' = Set(), + val newCorrectValues: Set[Set[Value]] = correctProcsMessages.map(m => m.values) + val newCrashedProcsValues: Set[Set[Value]] = crashedProcsMessages.map(m => m.values) + procState' = procState.keys().mapBy(p => { + // Find if this process is a target in any hiding config + val configForThisProc = hidingConfigs.filter(config => config.targetProc == p) + + val processedValues = + if (configForThisProc.size() > 0) { + // Get all processes that should be hidden from this process + val hiddenFromThis = flatten(configForThisProc.map(config => config.hiddenProcs)) + + // Filter out messages from hidden processes + val allowedCrashedMessages = crashedProcsMessages + .filter(m => not(hiddenFromThis.contains(m.sender))) + .map(m => m.values) + + newCorrectValues.union(allowedCrashedMessages) + } else { + // If process is not in hiding configs, it receives all messages + newCorrectValues.union(newCrashedProcsValues) + } + + { ...procState.get(p), S: processedValues } + }), + crashed' = crashed, + newlyCrashed' = newlyCrashed, + } + action step = any{ randCrash.then(sendMessages).then(receiveMessages).then(computeAction) } - /// we crash process p, and the set s does not receive p's messages - action stepHidePsMessagesFromS(p,s) = any{ - crashProcess(p).then(sendMessages).then(receiveMessage(s)).then(computeAction) - } + action stepWithMultipleHiding(hidingConfigs) = + crashProcessesFromConfig(hidingConfigs) + .then(sendMessages) + .then(receiveMessagesWithHiding(hidingConfigs)) + .then(computeAction) } module properValues { //quint run --main=properValues KSetAgreementConsensus.qnt - import KSetAgreementConsensus(N = 6, F = 4, actualFaults = 2, K = 2 ).* + import KSetAgreementConsensus(N = 8, F = 3, actualFaults = 3, K = 2).* run consensusRunTest = init @@ -247,18 +295,26 @@ module properValues { module badValues { //quint run KSetAgreementConsensus.qnt --main badValues --invariant kSetAgreement --max-steps 5 //quint test --main=badValues KSetAgreementConsensus.qnt - import KSetAgreementConsensus(N = 8, F = 4, actualFaults = 5, K = 2 ).* + import KSetAgreementConsensus(N = 8, F = 3, actualFaults = 4, K = 2).* run consensusRunTest = init .then((F/K + 1).reps(_ => step)) .expect(validity) + // Test scenario where processes decide on different values: + // - Process 6 doesn't receive from 1,2 => decides 3 + // - Process 5 doesn't receive from 1 => decides 2 + // - Process 8 doesn't receive from 3 => decides 1 + // - Process 7 doesn't receive from 1,2,3,4 => decides 5 run consensusDisagreementTest = initializeProcsStateWithDistinctValues - .then(stepHidePsMessagesFromS(1, Set(2,4))) - .then(stepHidePsMessagesFromS(3, Set(4))) - .then(stepHidePsMessagesFromS(5, Set(6))) + .then((F/K + 1).reps(_ => stepWithMultipleHiding(Set( + { hiddenProcs: Set(1, 2), targetProc: 6 }, + { hiddenProcs: Set(1), targetProc: 5 }, + { hiddenProcs: Set(3), targetProc: 8 }, + { hiddenProcs: Set(1, 2, 3, 4), targetProc: 7 } + )))) .expect(not(kSetAgreement)) } From f26a82625e1869c9fd0ff1c75bf3cb124d2398ac Mon Sep 17 00:00:00 2001 From: bugarela Date: Thu, 14 Nov 2024 09:25:20 -0300 Subject: [PATCH 4/4] Refactoring from group discussion --- .../ConsensusAlgorithm/ConsensusAlg.qnt | 102 ++++--- .../KSetAgreementConsensus.qnt | 268 ++---------------- 2 files changed, 90 insertions(+), 280 deletions(-) diff --git a/examples/classic/distributed/ConsensusAlgorithm/ConsensusAlg.qnt b/examples/classic/distributed/ConsensusAlgorithm/ConsensusAlg.qnt index 5ec88b227..a2ed7ebe2 100644 --- a/examples/classic/distributed/ConsensusAlgorithm/ConsensusAlg.qnt +++ b/examples/classic/distributed/ConsensusAlgorithm/ConsensusAlg.qnt @@ -12,6 +12,7 @@ module ConsensusAlg { const N : int const F : int const actualFaults : int + const MAX_ROUNDS : int type Proc = int type Value = int @@ -24,12 +25,14 @@ module ConsensusAlg { type LocalState = { V: Set[Value], - k: Round, + r: Round, y: Decision, S: Set[Set[Value]], x: Value } + type Stage = Starting | Sending | Receiving | Computing + // // Local functions // @@ -41,12 +44,12 @@ module ConsensusAlg { pure def compute(s: LocalState): LocalState = { val newV = s.V.union(flatten(s.S)) - val newK = s.k + 1 - val newY = if (newK == F + 1) Some(minValue(newV)) else s.y + val newR = s.r + 1 + val newY = if (newR == MAX_ROUNDS) Some(minValue(newV)) else s.y { V: newV, - k: newK, + r: newR, y: newY, S: Set(), x: s.x @@ -65,6 +68,7 @@ module ConsensusAlg { var procState: int -> LocalState var crashed: Set[int] var newlyCrashed: Set[int] + var stage: Stage // // Invariants @@ -96,7 +100,7 @@ module ConsensusAlg { nondet initialValues = Procs.setOfMaps(Set(1, 2, 3)).oneOf() procState' = Procs.mapBy(i => { V: Set(initialValues.get(i)), - k: 1, + r: 1, y: None, S: Set(), x: initialValues.get(i) @@ -105,13 +109,14 @@ module ConsensusAlg { correctProcsMessages' = Set(), crashed' = Set(), newlyCrashed' = Set(), - crashedProcsMessages' = Set() + crashedProcsMessages' = Set(), + stage' = Starting, } action initializeProcsStateWithDistinctValues = all { procState' = Procs.mapBy(i => { V: Set(i), - k: 1, + r: 1, y: None, S: Set(), x: i @@ -120,30 +125,28 @@ module ConsensusAlg { correctProcsMessages' = Set(), crashed' = Set(), newlyCrashed' = Set(), - crashedProcsMessages' = Set() + crashedProcsMessages' = Set(), } action sendMessages = all { - if (round <= F + 1) - correctProcsMessages' = Procs.exclude(crashed).exclude(newlyCrashed).map(p => { - sender: p, - values: procState.get(p).V - }) - else - correctProcsMessages' = correctProcsMessages, - if(newlyCrashed.size() > 0){ - crashedProcsMessages' = newlyCrashed.map(p => { - sender: p, - values: procState.get(p).V - }) - } else{ - crashedProcsMessages' = crashedProcsMessages - }, + correctProcsMessages' = Procs.exclude(crashed).exclude(newlyCrashed).map(p => { + sender: p, + values: procState.get(p).V + }), + crashedProcsMessages' = + if (newlyCrashed.size() > 0){ + newlyCrashed.map(p => { + sender: p, + values: procState.get(p).V + }) + } else{ + crashedProcsMessages + }, round' = round, procState' = procState, crashed' = crashed, - newlyCrashed' = newlyCrashed - } + newlyCrashed' = newlyCrashed, + } action crashProcess(p) = all { newlyCrashed' = Set(p), @@ -157,7 +160,8 @@ module ConsensusAlg { action randCrash = all { if (actualFaults - crashed.size() > 0) { nondet newCrashCount = oneOf(1.to(actualFaults - crashed.size())) - newlyCrashed' = Procs.exclude(crashed).powerset().filter(s => s.size() == newCrashCount).oneOf() + nondet newlyCrashedProcesses = Procs.exclude(crashed).powerset().filter(s => s.size() == newCrashCount).oneOf() + newlyCrashed' = newlyCrashedProcesses } else { newlyCrashed' = newlyCrashed }, @@ -191,7 +195,7 @@ module ConsensusAlg { round' = round + 1, crashed' = crashed.union(newlyCrashed), newlyCrashed' = Set(), - crashedProcsMessages' =Set() + crashedProcsMessages' = Set() } /// the set s of correct processes don't receive the messages from newlycrashed @@ -213,20 +217,33 @@ module ConsensusAlg { newlyCrashed' = newlyCrashed, } - action step = any{ - randCrash.then(sendMessages).then(receiveMessages).then(computeAction) - } - - /// we crash process p, and the set s does not receive p's messages - action stepHidePsMessagesFromS(p,s) = any{ - crashProcess(p).then(sendMessages).then(receiveMessage(s)).then(computeAction) + action stuttering = all { + round' = round, + correctProcsMessages' = correctProcsMessages, + crashedProcsMessages' = crashedProcsMessages, + procState' = procState, + crashed' = crashed, + newlyCrashed' = newlyCrashed, + stage' = stage, + } + + action step = + if (round > MAX_ROUNDS) { + stuttering + } else { + match stage { + | Starting => all { randCrash, stage' = Sending } + | Sending => all { sendMessages, stage' = Receiving } + | Receiving => all { receiveMessages, stage' = Computing } + | Computing => all { computeAction, stage' = Starting } + } } } module properValues { //quint run --main=properValues ConsensusAlg.qnt - import ConsensusAlg(N = 6, F = 1, actualFaults = 1 ).* + import ConsensusAlg(N = 6, F = 1, actualFaults = 1, MAX_ROUNDS = 2).* run consensusRunTest = init @@ -239,14 +256,19 @@ module properValues { module badValues { //quint run ConsensusAlg.qnt --main badValues --invariant agreement --max-steps 5 //quint test --main=badValues ConsensusAlg.qnt - import ConsensusAlg(N = 6, F = 1, actualFaults = 2 ).* + import ConsensusAlg(N = 6, F = 1, actualFaults = 2, MAX_ROUNDS = 2).* - run consensusRunTest = + run consensusRunTest = init .then((F + 1).reps(_ => step)) - .expect(validity) - - run consensusDisagreementTest = + .expect(validity) + + /// we crash process p, and the set s does not receive p's messages + run stepHidePsMessagesFromS(p,s) = any { + crashProcess(p).then(sendMessages).then(receiveMessage(s)).then(computeAction) + } + + run consensusDisagreementTest = initializeProcsStateWithDistinctValues .then(stepHidePsMessagesFromS(1, Set(2))) .then(stepHidePsMessagesFromS(3, Set(4))) diff --git a/examples/classic/distributed/ConsensusAlgorithm/KSetAgreementConsensus.qnt b/examples/classic/distributed/ConsensusAlgorithm/KSetAgreementConsensus.qnt index 1c06d4968..275575ba6 100644 --- a/examples/classic/distributed/ConsensusAlgorithm/KSetAgreementConsensus.qnt +++ b/examples/classic/distributed/ConsensusAlgorithm/KSetAgreementConsensus.qnt @@ -8,178 +8,40 @@ (* http://lib.ysu.am/disciplines_bk/c95d04e111f3e28ae4cc589bfda1e18b.pdf *) *******************************************************************************************************/ module KSetAgreementConsensus { + import ConsensusAlg.* from "ConsensusAlg" + export ConsensusAlg.* - const N : int - const F : int - const actualFaults : int const K : int - type Proc = int - type Value = int - type Round = int - type Message = { sender: Proc, values: Set[Value] } - - type Decision = - | None - | Some(Value) - - type LocalState = { - V: Set[Value], - r: Round, - y: Decision, - S: Set[Set[Value]], - x: Value - } - - type HiddenProcs = { - hiddenProcs: Set[Proc], // processes whose messages are hidden - targetProc: Proc // process from which messages are hidden - } - - // - // Local functions - // - - def getFirst(s: Set[int]): int = s.fold(0, (_, v) => v) - - def minValue(values: Set[int]): int = { val initial = getFirst(values) values.fold(initial, (min, v) => if (v < min) v else min) } - - pure def compute(s: LocalState): LocalState = { - - val newV = s.V.union(flatten(s.S)) - val newK = s.r + 1 - val newY = if (newK == F/K + 1) Some(minValue(newV)) else s.y - - { - V: newV, - r: newK, - y: newY, - S: Set(), - x: s.x - } - } - - // - // State machine - // - - val Procs: Set[int] = 1.to(N - 1) - - var round: Round - var correctProcsMessages: Set[Message] - var crashedProcsMessages: Set[Message] - var procState: int -> LocalState - var crashed: Set[int] - var newlyCrashed: Set[int] - - // - // Invariants - // - - def agreement = Procs.exclude(crashed).forall(p => - Procs.exclude(crashed).forall(q => - ( procState.get(p).y != None and procState.get(q).y != None) implies - procState.get(p).y == procState.get(q).y)) - def kSetAgreement = { // Get all decided values (excluding None) and ensure they are unique val decidedValues = Procs.exclude(crashed).map(p => procState.get(p).y).filter(v => v != None) - + // Check that number of unique decided values is at most K decidedValues.size() <= K } - /// If all processes have the same initial value v, then this must be the only decision value - def validity = - val allXValues = Procs.map(p => procState.get(p).x) - if (allXValues.size() == 1) - allXValues.forall(v => - Procs.exclude(crashed).forall(p => - match procState.get(p).y { - | Some(y) => y == v - | None => true - })) - else - true - - // - // Steps - // +} - action init = all { - nondet initialValues = Procs.setOfMaps(Set(1, 2, 3)).oneOf() - procState' = Procs.mapBy(i => { - V: Set(initialValues.get(i)), - r: 1, - y: None, - S: Set(), - x: initialValues.get(i) - }), - round' = 1, - correctProcsMessages' = Set(), - crashed' = Set(), - newlyCrashed' = Set(), - crashedProcsMessages' = Set() - } +module KSetProperValues { + //quint run --main=KSetProperValues KSetAgreementConsensus.qnt + import KSetAgreementConsensus(N = 8, F = 3, actualFaults = 3, K = 2, MAX_ROUNDS = (3/2 + 1)).* - action initializeProcsStateWithDistinctValues = all { - procState' = Procs.mapBy(i => { - V: Set(i), - r: 1, - y: None, - S: Set(), - x: i - }), - round' = 1, - correctProcsMessages' = Set(), - crashed' = Set(), - newlyCrashed' = Set(), - crashedProcsMessages' = Set() - } + run consensusRunTest = + init + .then((F/K + 1).reps(_ => step)) + .expect(kSetAgreement) + .expect(validity) +} - action sendMessages = all { - if (round <= F/K + 1) - correctProcsMessages' = Procs.exclude(crashed).exclude(newlyCrashed).map(p => { - sender: p, - values: procState.get(p).V - }) - else - correctProcsMessages' = correctProcsMessages, - if(newlyCrashed.size() > 0){ - crashedProcsMessages' = newlyCrashed.map(p => { - sender: p, - values: procState.get(p).V - }) - } else{ - crashedProcsMessages' = crashedProcsMessages - }, - round' = round, - procState' = procState, - crashed' = crashed, - newlyCrashed' = newlyCrashed - } +module KSetBadValues { + //quint run KSetAgreementConsensus.qnt --main KSetBadValues --invariant kSetAgreement --max-steps 5 + //quint test --main=KSetBadValues KSetAgreementConsensus.qnt + import KSetAgreementConsensus(N = 8, F = 3, actualFaults = 4, K = 2, MAX_ROUNDS = (3/2 + 1)).* - action crashProcess(p) = all { - newlyCrashed' = Set(p), - crashed' = crashed, - round' = round, - procState' = procState, - correctProcsMessages' = correctProcsMessages, - crashedProcsMessages' = crashedProcsMessages - } - - action randCrash = all { - if (actualFaults - crashed.size() > 0) { - nondet newCrashCount = oneOf(1.to(actualFaults - crashed.size())) - newlyCrashed' = Procs.exclude(crashed).powerset().filter(s => s.size() == newCrashCount).oneOf() - } else { - newlyCrashed' = newlyCrashed - }, - crashed' = crashed, - round' = round, - procState' = procState, - correctProcsMessages' = correctProcsMessages, - crashedProcsMessages' = crashedProcsMessages - } + run consensusRunTest = + init + .then((F/K + 1).reps(_ => step)) + .expect(validity) action crashProcessesFromConfig(hidingConfigs) = all { // Collect all processes that need to be crashed from all hiding configurations @@ -191,51 +53,6 @@ module KSetAgreementConsensus { crashedProcsMessages' = crashedProcsMessages } - action receiveMessages = all { - round' = round, - correctProcsMessages' = Set(), - crashedProcsMessages' = Set(), - val newCorrectValues: Set[Set[Value]] = correctProcsMessages.map(m => m.values) - if (crashedProcsMessages.size() == 0){ - procState' = procState.keys().mapBy(p => {... procState.get(p), S:newCorrectValues}) - } - else{ - val newCrashedProcsValues: Set[Set[Value]] = crashedProcsMessages.map(m => m.values) - nondet crashedMessagesRecived = Procs.setOfMaps(newCrashedProcsValues).union(Set()).oneOf()// for each process we pick from which newly crashed they receive a message - procState' = procState.keys().mapBy(p => { ... procState.get(p), S: newCorrectValues.union(Set(crashedMessagesRecived.get(p))) }) - }, - crashed' = crashed, - newlyCrashed' = newlyCrashed, - } - - action computeAction = all { - correctProcsMessages' = Set(), - procState' = procState.keys().mapBy(p => compute(procState.get(p))), - round' = round + 1, - crashed' = crashed.union(newlyCrashed), - newlyCrashed' = Set(), - crashedProcsMessages' =Set() - } - - /// the set s of correct processes don't receive the messages from newlycrashed - action receiveMessage(s) = all { - round' = round, - correctProcsMessages' = Set(), - crashedProcsMessages' = Set(), - val newCorrectValues: Set[Set[Value]] = correctProcsMessages.map(m => m.values) - val newCrashedProcsValues: Set[Set[Value]] = crashedProcsMessages.map(m => m.values) - procState' = procState.keys().mapBy(p => - { ...procState.get(p), - S: if (s.contains(p)) - newCorrectValues - else - newCorrectValues.union(newCrashedProcsValues) - } - ), - crashed' = crashed, - newlyCrashed' = newlyCrashed, - } - action receiveMessagesWithHiding(hidingConfigs) = all { round' = round, correctProcsMessages' = Set(), @@ -245,69 +62,41 @@ module KSetAgreementConsensus { procState' = procState.keys().mapBy(p => { // Find if this process is a target in any hiding config val configForThisProc = hidingConfigs.filter(config => config.targetProc == p) - - val processedValues = + + val processedValues = if (configForThisProc.size() > 0) { // Get all processes that should be hidden from this process val hiddenFromThis = flatten(configForThisProc.map(config => config.hiddenProcs)) - + // Filter out messages from hidden processes val allowedCrashedMessages = crashedProcsMessages .filter(m => not(hiddenFromThis.contains(m.sender))) .map(m => m.values) - + newCorrectValues.union(allowedCrashedMessages) } else { // If process is not in hiding configs, it receives all messages newCorrectValues.union(newCrashedProcsValues) } - + { ...procState.get(p), S: processedValues } }), crashed' = crashed, newlyCrashed' = newlyCrashed, } - action step = any{ - randCrash.then(sendMessages).then(receiveMessages).then(computeAction) - } - - action stepWithMultipleHiding(hidingConfigs) = + run stepWithMultipleHiding(hidingConfigs) = crashProcessesFromConfig(hidingConfigs) .then(sendMessages) .then(receiveMessagesWithHiding(hidingConfigs)) .then(computeAction) -} - -module properValues { - //quint run --main=properValues KSetAgreementConsensus.qnt - import KSetAgreementConsensus(N = 8, F = 3, actualFaults = 3, K = 2).* - - run consensusRunTest = - init - .then((F/K + 1).reps(_ => step)) - .expect(kSetAgreement) - .expect(validity) -} - - -module badValues { - //quint run KSetAgreementConsensus.qnt --main badValues --invariant kSetAgreement --max-steps 5 - //quint test --main=badValues KSetAgreementConsensus.qnt - import KSetAgreementConsensus(N = 8, F = 3, actualFaults = 4, K = 2).* - - run consensusRunTest = - init - .then((F/K + 1).reps(_ => step)) - .expect(validity) - // Test scenario where processes decide on different values: // - Process 6 doesn't receive from 1,2 => decides 3 // - Process 5 doesn't receive from 1 => decides 2 // - Process 8 doesn't receive from 3 => decides 1 // - Process 7 doesn't receive from 1,2,3,4 => decides 5 - run consensusDisagreementTest = + run consensusDisagreementTest = initializeProcsStateWithDistinctValues .then((F/K + 1).reps(_ => stepWithMultipleHiding(Set( { hiddenProcs: Set(1, 2), targetProc: 6 }, @@ -316,5 +105,4 @@ module badValues { { hiddenProcs: Set(1, 2, 3, 4), targetProc: 7 } )))) .expect(not(kSetAgreement)) - }