From d131cd8c8bc04d91b23f698c64dfc30d7f19487b Mon Sep 17 00:00:00 2001 From: lasarojc Date: Fri, 16 Jun 2023 07:58:24 -0300 Subject: [PATCH 01/19] Debug socket based apps in local testnet --- howtos/debug-k8-testnet.md | 44 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 howtos/debug-k8-testnet.md diff --git a/howtos/debug-k8-testnet.md b/howtos/debug-k8-testnet.md new file mode 100644 index 0000000..5af67d8 --- /dev/null +++ b/howtos/debug-k8-testnet.md @@ -0,0 +1,44 @@ +# Local testnet debug + +## Remote app + +1. Build the docker debug image + + ```bash + make build-linux + cd test/e2e + make docker-debug generator runner + ``` + +2. Generate your manifest normally. +3. Start your run + + ```bash + ./build/runner -f networks/testnet.toml setup + ./build/runner -f networks/testnet.toml start + ``` + +4. Figure out the ports exported by docker on each container + + ```bash + docker container ls --format "table {{.ID}}\t{{.Names}}\t{{.Ports}}" -a + ``` + + In the following example, on `validator01` the app debugger is listening on 51600 `(0.0.0.0:51600->2345/tcp)` and Comet will listen on 51601 `(0.0.0.0:51601->2346/tcp)`. + + ```bash + CONTAINER ID NAMES PORTS +f87ebb9ab8d8 validator01 26660/tcp, 0.0.0.0:51600->2345/tcp, 0.0.0.0:51601->2346/tcp, 0.0.0.0:51603->6060/tcp, 0.0.0.0:51602->26656/tcp, 0.0.0.0:5703->26657/tcp +1973cd2be79a validator02 26660/tcp, 0.0.0.0:51598->2345/tcp, 0.0.0.0:51599->2346/tcp, 0.0.0.0:51597->6060/tcp, 0.0.0.0:51596->26656/tcp, 0.0.0.0:5704->26657/tcp +a213c8e53b90 validator03 26660/tcp, 0.0.0.0:51605->2345/tcp, 0.0.0.0:51606->2346/tcp, 0.0.0.0:51608->6060/tcp, 0.0.0.0:51607->26656/tcp, 0.0.0.0:5701->26657/tcp + ``` + +5. Connect with a debugger to the app. + - Beware that once you let the app run, it will try to connect to the signer service for a few seconds, so quickly move to the next step. + +6. Connect to CometBFT + +## Built-in app + +1. Use the Dockerfile.debug-builtin +... From d784c7ef4f9b4b866efb59d113d35d6162def70c Mon Sep 17 00:00:00 2001 From: lasarojc Date: Tue, 24 Oct 2023 14:55:16 -0400 Subject: [PATCH 02/19] first --- generic multicast/gmcast0.qnt | 42 +++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 generic multicast/gmcast0.qnt diff --git a/generic multicast/gmcast0.qnt b/generic multicast/gmcast0.qnt new file mode 100644 index 0000000..4b442bf --- /dev/null +++ b/generic multicast/gmcast0.qnt @@ -0,0 +1,42 @@ +module gmcast0 { + type ProcId = int + + //XXX Quint: Ideally these should be consts, but because it would have to be instantiated on every import, there would be duplication. + //All processes in the system + + pure val MsgType = Set("S0", "S1", "S2") + pure val ProcIds = Set(1,2,3,4,5) + type Message = { + tag: Set[string], //Shoud be MsgType + src: ProcId, + dst: ProcId + } + + //Nodes keep the following state + type Node = { + k: ProcId => int, + pending: ProcId => Set[(Message)], + delivering: ProcId => Set[(Message)], + delivered: ProcId => Set[(Message)], + previous: ProcId => Set[(Message)] + } + + type Network = { + msgsSent: Set[(Message)], //Unicast sent messages. + msgsRcvd: Set[(Message)], //Unicast received messages + } + + + var nodeState: ProcId -> NodeState + var networkState: Network + + action init: bool = all { + nodeState' = { + ProcIds.mapBy(p => 0) + + + + }, + networkState' = {msgsSent: Set(), msgsRcvd: Set()} + } +} \ No newline at end of file From d76da2a02b0bb79d99c723ebc07c32b54801033a Mon Sep 17 00:00:00 2001 From: lasarojc Date: Tue, 24 Oct 2023 14:55:44 -0400 Subject: [PATCH 03/19] first --- generic multicast/skeen.qnt | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 generic multicast/skeen.qnt diff --git a/generic multicast/skeen.qnt b/generic multicast/skeen.qnt new file mode 100644 index 0000000..821039a --- /dev/null +++ b/generic multicast/skeen.qnt @@ -0,0 +1,27 @@ +module skeen { + type ProcId = int + + //XXX Quint: Ideally this should be a const, but because it would have to be instantiated on every import, there would be duplication. + //All processes in the system + pure val ProcIds = Set(1,2,3,4,5) + + //Nodes are fully connected + + //Nodes keep the following state + type NodeState = { + } + + type NetworkState = { + msgsSent: Set[{src:ProcId, dst:ProcId}], //Unicast sent messages. + msgsRcvd: Set[{src:ProcId, dst:ProcId}], //Unicast received messages + } + + var pid2nodeState: ProcId -> NodeState + + action init: bool = all { + pid2nodeState' = ProcIds.mapBy(p => { + + }), + networkState' = {msgsSent: Set(), msgsRcvd: Set()} + } +} \ No newline at end of file From a7e7c7d58f2e78c5d2f210916c96ab815df224b0 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Tue, 24 Oct 2023 15:38:10 -0400 Subject: [PATCH 04/19] Implement GMSend --- generic multicast/gmcast0.qnt | 42 ---------- genericMulticast/gmcast0.qnt | 83 +++++++++++++++++++ .../skeen.qnt | 0 genericMulticast/spells.qnt | 6 ++ 4 files changed, 89 insertions(+), 42 deletions(-) delete mode 100644 generic multicast/gmcast0.qnt create mode 100644 genericMulticast/gmcast0.qnt rename {generic multicast => genericMulticast}/skeen.qnt (100%) create mode 100644 genericMulticast/spells.qnt diff --git a/generic multicast/gmcast0.qnt b/generic multicast/gmcast0.qnt deleted file mode 100644 index 4b442bf..0000000 --- a/generic multicast/gmcast0.qnt +++ /dev/null @@ -1,42 +0,0 @@ -module gmcast0 { - type ProcId = int - - //XXX Quint: Ideally these should be consts, but because it would have to be instantiated on every import, there would be duplication. - //All processes in the system - - pure val MsgType = Set("S0", "S1", "S2") - pure val ProcIds = Set(1,2,3,4,5) - type Message = { - tag: Set[string], //Shoud be MsgType - src: ProcId, - dst: ProcId - } - - //Nodes keep the following state - type Node = { - k: ProcId => int, - pending: ProcId => Set[(Message)], - delivering: ProcId => Set[(Message)], - delivered: ProcId => Set[(Message)], - previous: ProcId => Set[(Message)] - } - - type Network = { - msgsSent: Set[(Message)], //Unicast sent messages. - msgsRcvd: Set[(Message)], //Unicast received messages - } - - - var nodeState: ProcId -> NodeState - var networkState: Network - - action init: bool = all { - nodeState' = { - ProcIds.mapBy(p => 0) - - - - }, - networkState' = {msgsSent: Set(), msgsRcvd: Set()} - } -} \ No newline at end of file diff --git a/genericMulticast/gmcast0.qnt b/genericMulticast/gmcast0.qnt new file mode 100644 index 0000000..5dea356 --- /dev/null +++ b/genericMulticast/gmcast0.qnt @@ -0,0 +1,83 @@ +module gmcast0 { + type ProcId = int + + //XXX Quint: Ideally these should be consts, but because it would have to be instantiated on every import, there would be duplication. + //All processes in the system + + pure val MsgType = Set("S0", "S1", "S2") + pure val ProcIds = Set(1,2,3,4,5) + type Message = { + tag: str, //Shoud be in MsgType + timestamp: int, // -1 means no timestamp + channel: (ProcId, ProcId), // (sender, receiver) + // groups of processes this message goes to + dst: Set[Set[ProcId]], + payload: str + } + + pure val Groups = Set( + Set(1,2), + Set(3,4), + Set(5) + ) + + //Nodes keep the following state + type NodeState = { + k: int, + pending: Set[Message], + delivering: Set[Message], + delivered: Set[Message], + previous: Set[Message] + } + + type Network = { + // ProcId is the receiver of the message + msgsSent: Set[Message], //Unicast sent messages. + msgsRcvd: Set[Message], //Unicast received messages + } + + + var nodeState: ProcId -> NodeState + var networkState: Network + + // action init: bool = all { + // nodeState' = ProcIds.mapBy( + // p => { + // k: 0, + // pending: Set(), + // delivering: Set(), + // delivered: Set(), + // previous: Set() + // }), + // networkState' = {msgsSent: Set(), msgsRcvd: Map()} + // } + + action GMSend(sender: ProcId, payload: str, groups: Set[Set[ProcId]]): bool = { + all { + // the groups are a valid destination for the multicast + groups.forall(group => Groups.contains(group)), + // construct the message + val message = { + tag: "S0", + timestamp: -1, + channel: (-1, -1), // will be filled below + dst: groups, + payload: payload + } + val receivers = groups.flatten() + val newMsgsSent = + receivers.fold( + Set(), + (acc, receiver) => + acc.union(Set( + { + channel: (sender, receiver), + ...message + } + ) + ) + ) + networkState' = {msgsSent: newMsgsSent, ...networkState} + } + } +} \ No newline at end of file diff --git a/generic multicast/skeen.qnt b/genericMulticast/skeen.qnt similarity index 100% rename from generic multicast/skeen.qnt rename to genericMulticast/skeen.qnt diff --git a/genericMulticast/spells.qnt b/genericMulticast/spells.qnt new file mode 100644 index 0000000..3900454 --- /dev/null +++ b/genericMulticast/spells.qnt @@ -0,0 +1,6 @@ +module spells { + + pure def flatten(__in: Set[Set[__a]]): Set[__a] = { + __in.fold(Set.empty[__a])((acc, s) => acc.union(s)) + } +} \ No newline at end of file From add4f12c18e862e31f4747e24ef239ee19ebd4e5 Mon Sep 17 00:00:00 2001 From: lasarojc Date: Tue, 24 Oct 2023 16:06:07 -0400 Subject: [PATCH 05/19] first test --- genericMulticast/gmcast0.qnt | 30 ++++++++++++++++++------------ genericMulticast/skeen.qnt | 27 --------------------------- genericMulticast/spells.qnt | 6 ------ genericMulticast/tests.qnt | 16 ++++++++++++++++ 4 files changed, 34 insertions(+), 45 deletions(-) delete mode 100644 genericMulticast/skeen.qnt delete mode 100644 genericMulticast/spells.qnt create mode 100644 genericMulticast/tests.qnt diff --git a/genericMulticast/gmcast0.qnt b/genericMulticast/gmcast0.qnt index 5dea356..122ef93 100644 --- a/genericMulticast/gmcast0.qnt +++ b/genericMulticast/gmcast0.qnt @@ -40,17 +40,22 @@ module gmcast0 { var nodeState: ProcId -> NodeState var networkState: Network - // action init: bool = all { - // nodeState' = ProcIds.mapBy( - // p => { - // k: 0, - // pending: Set(), - // delivering: Set(), - // delivered: Set(), - // previous: Set() - // }), - // networkState' = {msgsSent: Set(), msgsRcvd: Map()} - // } + action init: bool = all { + nodeState' = ProcIds.mapBy( + p => { + k: 0, + pending: Set(), + delivering: Set(), + delivered: Set(), + previous: Set() + }), + networkState' = {msgsSent: Set(), msgsRcvd: Set()} + } + + action unchanged_all: bool = all { + networkState' = networkState, + nodeState' = nodeState + } action GMSend(sender: ProcId, payload: str, groups: Set[Set[ProcId]]): bool = { all { @@ -77,7 +82,8 @@ module gmcast0 { ) ) ) - networkState' = {msgsSent: newMsgsSent, ...networkState} + networkState' = {msgsSent: newMsgsSent, ...networkState}, + nodeState' = nodeState } } } \ No newline at end of file diff --git a/genericMulticast/skeen.qnt b/genericMulticast/skeen.qnt deleted file mode 100644 index 821039a..0000000 --- a/genericMulticast/skeen.qnt +++ /dev/null @@ -1,27 +0,0 @@ -module skeen { - type ProcId = int - - //XXX Quint: Ideally this should be a const, but because it would have to be instantiated on every import, there would be duplication. - //All processes in the system - pure val ProcIds = Set(1,2,3,4,5) - - //Nodes are fully connected - - //Nodes keep the following state - type NodeState = { - } - - type NetworkState = { - msgsSent: Set[{src:ProcId, dst:ProcId}], //Unicast sent messages. - msgsRcvd: Set[{src:ProcId, dst:ProcId}], //Unicast received messages - } - - var pid2nodeState: ProcId -> NodeState - - action init: bool = all { - pid2nodeState' = ProcIds.mapBy(p => { - - }), - networkState' = {msgsSent: Set(), msgsRcvd: Set()} - } -} \ No newline at end of file diff --git a/genericMulticast/spells.qnt b/genericMulticast/spells.qnt deleted file mode 100644 index 3900454..0000000 --- a/genericMulticast/spells.qnt +++ /dev/null @@ -1,6 +0,0 @@ -module spells { - - pure def flatten(__in: Set[Set[__a]]): Set[__a] = { - __in.fold(Set.empty[__a])((acc, s) => acc.union(s)) - } -} \ No newline at end of file diff --git a/genericMulticast/tests.qnt b/genericMulticast/tests.qnt new file mode 100644 index 0000000..205c27e --- /dev/null +++ b/genericMulticast/tests.qnt @@ -0,0 +1,16 @@ +module tests { + import gmcast0.* from "./gmcast0" + + run GMSendTest: bool = { + init.then( + GMSend(1, "nada", Groups) + ).then( + all { + Groups.flatten().forall(p => networkState + .msgsSent + .exists(m => m.channel == (1,p))), + unchanged_all + } + ) + } +} \ No newline at end of file From ec5aec3a2808160b4e0cfc7b011f61f5d52c39ee Mon Sep 17 00:00:00 2001 From: lasarojc Date: Tue, 24 Oct 2023 16:16:24 -0400 Subject: [PATCH 06/19] send --- genericMulticast/gmcast0.qnt | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/genericMulticast/gmcast0.qnt b/genericMulticast/gmcast0.qnt index 122ef93..01a0239 100644 --- a/genericMulticast/gmcast0.qnt +++ b/genericMulticast/gmcast0.qnt @@ -40,6 +40,8 @@ module gmcast0 { var nodeState: ProcId -> NodeState var networkState: Network + pure def conflicts(lhs: Message, rhs: Message): bool = true + action init: bool = all { nodeState' = ProcIds.mapBy( p => { @@ -86,4 +88,15 @@ module gmcast0 { nodeState' = nodeState } } + + pure def GMReceiveHelper(m: Message, netState: NetworkState, noState: NodeState): (NetworkState,NodeState) { + + } + + /* + action GMReceive(m: Message): bool = all { + + networkState' = deliver(m), + nodeState' = nodeState + }*/ } \ No newline at end of file From 7de0a7ee95ed363fe4e674ecb8c8b64ba1b9eaee Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Tue, 24 Oct 2023 17:16:34 -0400 Subject: [PATCH 07/19] Add crossproduct spell --- genericMulticast/spell.qnt | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 genericMulticast/spell.qnt diff --git a/genericMulticast/spell.qnt b/genericMulticast/spell.qnt new file mode 100644 index 0000000..5f8ba45 --- /dev/null +++ b/genericMulticast/spell.qnt @@ -0,0 +1,18 @@ +module spell { + pure def crossproduct(__s1: Set[a], __s2: Set[b]): Set[(a, b)] = + __s1.fold( + Set(), + (acc1, a) => acc1.union(__s2.fold( + Set(), + (acc2, b) => acc2.union(Set((a, b))) + )) + ) + + run crossproductTest = { + all { + crossproduct(Set(1, 2), Set("a", "b")) == Set((1, "a"), (1, "b"), (2, "a"), (2, "b")), + crossproduct(Set(1, 2), Set()) == Set(), + crossproduct(Set(), Set()) == Set(), + } + } +} \ No newline at end of file From 9029e4a5a52f8651043aa7c4bf27c9b92ad9ee89 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Tue, 24 Oct 2023 17:31:32 -0400 Subject: [PATCH 08/19] Refactor network state --- genericMulticast/gmcast0.qnt | 81 ++++++++++++++++++++++-------------- genericMulticast/tests.qnt | 9 ++-- 2 files changed, 54 insertions(+), 36 deletions(-) diff --git a/genericMulticast/gmcast0.qnt b/genericMulticast/gmcast0.qnt index 01a0239..928a7de 100644 --- a/genericMulticast/gmcast0.qnt +++ b/genericMulticast/gmcast0.qnt @@ -1,4 +1,6 @@ module gmcast0 { + import spell.* from "./spell" + type ProcId = int //XXX Quint: Ideally these should be consts, but because it would have to be instantiated on every import, there would be duplication. @@ -9,12 +11,13 @@ module gmcast0 { type Message = { tag: str, //Shoud be in MsgType timestamp: int, // -1 means no timestamp - channel: (ProcId, ProcId), // (sender, receiver) // groups of processes this message goes to dst: Set[Set[ProcId]], - payload: str + id: int } + type Channel = (ProcId, ProcId) + pure val Groups = Set( Set(1,2), Set(3,4), @@ -30,11 +33,8 @@ module gmcast0 { previous: Set[Message] } - type Network = { - // ProcId is the receiver of the message - msgsSent: Set[Message], //Unicast sent messages. - msgsRcvd: Set[Message], //Unicast received messages - } + type Network = + Channel -> Set[Message] var nodeState: ProcId -> NodeState @@ -51,7 +51,11 @@ module gmcast0 { delivered: Set(), previous: Set() }), - networkState' = {msgsSent: Set(), msgsRcvd: Set()} + // create channels between all processes + networkState' = + ProcIds.crossproduct(ProcIds).mapBy( + (p1, p2) => Set() + ) } action unchanged_all: bool = all { @@ -59,44 +63,57 @@ module gmcast0 { nodeState' = nodeState } - action GMSend(sender: ProcId, payload: str, groups: Set[Set[ProcId]]): bool = { + action GMSend(sender: ProcId, id: int, groups: Set[Set[ProcId]]): bool = { all { // the groups are a valid destination for the multicast groups.forall(group => Groups.contains(group)), // construct the message val message = { tag: "S0", - timestamp: -1, - channel: (-1, -1), // will be filled below + timestamp: -1, // not used for S0 messages dst: groups, - payload: payload + id: id } val receivers = groups.flatten() val newMsgsSent = - receivers.fold( - Set(), - (acc, receiver) => - acc.union(Set( - { - channel: (sender, receiver), - ...message - } - ) - ) + ProcIds.crossproduct(ProcIds).mapBy( + (p1, p2) => Set() ) - networkState' = {msgsSent: newMsgsSent, ...networkState}, + networkState' = + networkState.keys().mapBy( + channel => + if (channel._1 == sender and receivers.contains(channel._2)) { + networkState.get(channel).union(Set(message)) + } else { + networkState.get(channel) + } + ), nodeState' = nodeState } } - - pure def GMReceiveHelper(m: Message, netState: NetworkState, noState: NodeState): (NetworkState,NodeState) { - } - - /* - action GMReceive(m: Message): bool = all { + // action ComputeSeqNumber(p: ProcId, m: Message): bool = { + // all { + // // for each destination process, we have received an S1 + // m.dst.flatten().forall( + // receiver => + // networkState.msgsRcvd.exists( + // msg => msg.channel == (p, receiver) and + // equal(msg, m) and + // msg.tag == "S1" + // ) + // ), + // // find the maximal timestamp among the S1 messages + // m.dst.flatten().fold( + // -1, + // (acc, receiver) => + // val msgFromReceiver = networkState.msgsRcvd.filter( + // msg => msg.channel == (p, receiver) and + // equal(msg, m) and + // msg.tag == "S1" + // ).chooseSome() + // ) - networkState' = deliver(m), - nodeState' = nodeState - }*/ + // } + // } } \ No newline at end of file diff --git a/genericMulticast/tests.qnt b/genericMulticast/tests.qnt index 205c27e..9ea711f 100644 --- a/genericMulticast/tests.qnt +++ b/genericMulticast/tests.qnt @@ -3,12 +3,13 @@ module tests { run GMSendTest: bool = { init.then( - GMSend(1, "nada", Groups) + GMSend(1, 0, Groups) ).then( all { - Groups.flatten().forall(p => networkState - .msgsSent - .exists(m => m.channel == (1,p))), + Groups.flatten().forall(p => + networkState.get((1, p)).exists( + msg => msg.id == 0 + )), unchanged_all } ) From 12266928429303e9e96a25fc02f8db54dbfab0d3 Mon Sep 17 00:00:00 2001 From: lasarojc Date: Tue, 24 Oct 2023 17:32:01 -0400 Subject: [PATCH 09/19] receive message --- genericMulticast/gmcast0.qnt | 41 +++++++++++++++++++++++++++++++++--- 1 file changed, 38 insertions(+), 3 deletions(-) diff --git a/genericMulticast/gmcast0.qnt b/genericMulticast/gmcast0.qnt index 928a7de..8d84ee2 100644 --- a/genericMulticast/gmcast0.qnt +++ b/genericMulticast/gmcast0.qnt @@ -27,7 +27,7 @@ module gmcast0 { //Nodes keep the following state type NodeState = { k: int, - pending: Set[Message], + pending: Set[(Message,int)], delivering: Set[Message], delivered: Set[Message], previous: Set[Message] @@ -114,6 +114,41 @@ module gmcast0 { // ).chooseSome() // ) - // } - // } + pure def GMReceiveHelper( + receiver: ProcId, + sender: ProcId, + m: Message, + netState: Network, + noState: NodeState + ): (Network, NodeState) = { + + val newK = + if (noState.previous.exists(om => om.conflicts(m))) + noState.k + 1 + else + noState.k + + val newPrevious = + if (noState.previous.exists(om => om.conflicts(m))) + Set(m) + else + noState.previous.union(Set(m)) + + val newPending = noState.pending.union(Set((m,newK))) + + val newNodeState = { + k: newK, + pending: newPending, + previous: newPrevious, + ...noState + } + + val newMsg = {tag: "S1", timestamp: newK, ...m} + + val newMsgsSent = netState.get((receiver,sender)).exclude(Set(m)).union(Set(newMsg)) + + val newNetworkState = netState.put((receiver, sender), newMsgsSent) + + (newNetworkState, newNodeState) + } } \ No newline at end of file From 1822d1a843a228292c5168770b89de4180383eed Mon Sep 17 00:00:00 2001 From: lasarojc Date: Wed, 25 Oct 2023 14:53:55 -0400 Subject: [PATCH 10/19] assign timestamp --- genericMulticast/gmcast0.qnt | 29 ++++++++++++++++++++++++++--- 1 file changed, 26 insertions(+), 3 deletions(-) diff --git a/genericMulticast/gmcast0.qnt b/genericMulticast/gmcast0.qnt index 8d84ee2..4fe8fc7 100644 --- a/genericMulticast/gmcast0.qnt +++ b/genericMulticast/gmcast0.qnt @@ -114,9 +114,9 @@ module gmcast0 { // ).chooseSome() // ) - pure def GMReceiveHelper( - receiver: ProcId, + pure def AssignTimestampHelper( sender: ProcId, + receiver: ProcId, m: Message, netState: Network, noState: NodeState @@ -145,10 +145,33 @@ module gmcast0 { val newMsg = {tag: "S1", timestamp: newK, ...m} - val newMsgsSent = netState.get((receiver,sender)).exclude(Set(m)).union(Set(newMsg)) + val newMsgsSent = netState.get((receiver,sender)).exclude(Set(m)).union(Set(newMsg)) //This is incomplete. val newNetworkState = netState.put((receiver, sender), newMsgsSent) (newNetworkState, newNodeState) } + + action AssignTimestamp(): bool = all { + val s0channels = networkState.keys() + .filter( k => + val src = k._1 + val dst = k._2 + networkState.get(k).exists(m => m.tag == "S0")) + all { + s0channels.size() > 0, + nondet s0channel = s0channels.oneOf() + val sender = s0channel._1 + val receiver = s0channel._2 + val receiverState = nodeState.get(s0channel._2) + nondet s0msg = networkState.get(s0channel).filter(m => m.tag == "S0").oneOf() + val newState = AssignTimestampHelper(sender, receiver, s0msg, networkState, receiverState) + val newNetworkState = newState._1 + val newReceiverState = newState._2 + all { + networkState' = newNetworkState, + nodeState' = nodeState.put(receiver, newReceiverState) + } + } + } } \ No newline at end of file From 47bfc2c5b0c0b78234db4d3f663f03aea52e8df5 Mon Sep 17 00:00:00 2001 From: lasarojc Date: Wed, 25 Oct 2023 16:18:25 -0400 Subject: [PATCH 11/19] no longer incomplete --- genericMulticast/gmcast0.qnt | 25 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) diff --git a/genericMulticast/gmcast0.qnt b/genericMulticast/gmcast0.qnt index 4fe8fc7..7004abf 100644 --- a/genericMulticast/gmcast0.qnt +++ b/genericMulticast/gmcast0.qnt @@ -145,26 +145,21 @@ module gmcast0 { val newMsg = {tag: "S1", timestamp: newK, ...m} - val newMsgsSent = netState.get((receiver,sender)).exclude(Set(m)).union(Set(newMsg)) //This is incomplete. - - val newNetworkState = netState.put((receiver, sender), newMsgsSent) + val newIncomingChannel = netState.get((sender,receiver)).exclude(Set(m)) + val newOutgoingChannel = if (sender == receiver) + newIncomingChannel.union(Set(newMsg)) + else + netState.get((receiver,sender)).union(Set(newMsg)) + val newNetworkState = + netState.put((sender,receiver), newIncomingChannel) + .put((receiver, sender), newOutgoingChannel) (newNetworkState, newNodeState) } - action AssignTimestamp(): bool = all { - val s0channels = networkState.keys() - .filter( k => - val src = k._1 - val dst = k._2 - networkState.get(k).exists(m => m.tag == "S0")) + action AssignTimestamp(sender: ProcId, receiver: ProcId, s0msg: Message): bool = all { all { - s0channels.size() > 0, - nondet s0channel = s0channels.oneOf() - val sender = s0channel._1 - val receiver = s0channel._2 - val receiverState = nodeState.get(s0channel._2) - nondet s0msg = networkState.get(s0channel).filter(m => m.tag == "S0").oneOf() + val receiverState = nodeState.get(receiver) val newState = AssignTimestampHelper(sender, receiver, s0msg, networkState, receiverState) val newNetworkState = newState._1 val newReceiverState = newState._2 From a88ebf1c9fce7a667a5940381d94bdcc0f9b70b0 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Wed, 25 Oct 2023 16:26:25 -0400 Subject: [PATCH 12/19] Add ComputeSeqNumber --- genericMulticast/gmcast0.qnt | 72 +++++++++++++++++++++++++----------- genericMulticast/tests.qnt | 21 +++++++++++ 2 files changed, 72 insertions(+), 21 deletions(-) diff --git a/genericMulticast/gmcast0.qnt b/genericMulticast/gmcast0.qnt index 4fe8fc7..57db58a 100644 --- a/genericMulticast/gmcast0.qnt +++ b/genericMulticast/gmcast0.qnt @@ -92,27 +92,57 @@ module gmcast0 { } } - // action ComputeSeqNumber(p: ProcId, m: Message): bool = { - // all { - // // for each destination process, we have received an S1 - // m.dst.flatten().forall( - // receiver => - // networkState.msgsRcvd.exists( - // msg => msg.channel == (p, receiver) and - // equal(msg, m) and - // msg.tag == "S1" - // ) - // ), - // // find the maximal timestamp among the S1 messages - // m.dst.flatten().fold( - // -1, - // (acc, receiver) => - // val msgFromReceiver = networkState.msgsRcvd.filter( - // msg => msg.channel == (p, receiver) and - // equal(msg, m) and - // msg.tag == "S1" - // ).chooseSome() - // ) + action ComputeSeqNumber(p: ProcId, id: int, dst: Set[Set[ProcId]]): bool = { + all { + // for all processes in dst, we have received an S1 + dst.flatten().forall( + receiver => + // there must be a message tagged with S1 sent by receiver to p relating to m + networkState.get((p, receiver)).exists( + msg => msg.id == id and + msg.tag == "S1" + ) + + ), + // get messages tagged with S1 received by p relating to the message id + val receivedMessages = dst.flatten().fold( + Set(), (acc, receiver) => + val msgsFromReceiver = networkState.get((receiver, p)).filter( + msg => msg.id == id and + msg.tag == "S1") + acc.union(msgsFromReceiver) + ) + + // find the maximal timestamp among the S1 messages + val timestamp_final = receivedMessages.fold( + -1, + (acc, msg) => + if (msg.timestamp > acc) { + msg.timestamp + } else { + acc + } + ) + // tag the message with S2 and the timestamp + val message_final = { + tag: "S2", + timestamp: timestamp_final, + dst: dst, + id: id + } + // send it to all destination processes + networkState' = + networkState.keys().mapBy( + channel => + if (dst.flatten().contains(channel._2)) { + networkState.get(channel).union(Set(message_final)) + } else { + networkState.get(channel) + } + ), + nodeState' = nodeState + } + } pure def AssignTimestampHelper( sender: ProcId, diff --git a/genericMulticast/tests.qnt b/genericMulticast/tests.qnt index 9ea711f..46ad96d 100644 --- a/genericMulticast/tests.qnt +++ b/genericMulticast/tests.qnt @@ -14,4 +14,25 @@ module tests { } ) } + + run ComputeSeqNumberTest: bool = { + GMSendTest.then( + // everyone assigns a timestamp + ProcIds.size().reps(i => AssignTimestamp) + ).then( + // everyone computes a sequence number + ComputeSeqNumber( + 1, 0, Groups + ) + ).then( + all { + // 1 sent a message with the same timestamp to everyone + Groups.flatten().forall(p => + networkState.get((1, p)).exists( + msg => msg.id == 0 and msg.timestamp == 0 and msg.tag == "S2" + )), + unchanged_all + } + ) + } } \ No newline at end of file From 5ac67c5471d8e7b7d69b1fecef8f2a985a3a1d85 Mon Sep 17 00:00:00 2001 From: lasarojc Date: Wed, 25 Oct 2023 16:28:27 -0400 Subject: [PATCH 13/19] tests for assign timestamp --- genericMulticast/tests.qnt | 29 ++++++++++++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) diff --git a/genericMulticast/tests.qnt b/genericMulticast/tests.qnt index 46ad96d..b3adf8f 100644 --- a/genericMulticast/tests.qnt +++ b/genericMulticast/tests.qnt @@ -35,4 +35,31 @@ module tests { } ) } -} \ No newline at end of file + + run GMReceiveTest: bool = { + init.then( + GMSend(1, 0, Groups) + ).then( + nondet s0channel = networkState.keys() + .filter( k => + val src = k._1 + val dst = k._2 + networkState.get(k).exists(m => m.tag == "S0")).oneOf() + val sender = s0channel._1 + val receiver = s0channel._2 + val receiverState = nodeState.get(receiver) + nondet s0msg = networkState.get(s0channel).filter(m => m.tag == "S0").oneOf() + AssignTimestamp(sender, receiver, s0msg).then( + all { + networkState.get((receiver, sender)).exists( + msg => all { + msg.id == 0, + msg.tag == "S1" + } + ), + unchanged_all + } + ) + ) + } +} From 24b892f81bb22d79b32fd3e3b8d89a955233053d Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Wed, 25 Oct 2023 16:44:01 -0400 Subject: [PATCH 14/19] Add test for ComputeSeqNumber --- genericMulticast/tests.qnt | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/genericMulticast/tests.qnt b/genericMulticast/tests.qnt index b3adf8f..80fd6f8 100644 --- a/genericMulticast/tests.qnt +++ b/genericMulticast/tests.qnt @@ -18,7 +18,15 @@ module tests { run ComputeSeqNumberTest: bool = { GMSendTest.then( // everyone assigns a timestamp - ProcIds.size().reps(i => AssignTimestamp) + val procIdList = ProcIds.fold( + List(), + (acc, p) => acc.append(p) + ) + procIdList.length().reps( + i => AssignTimestamp( + procIdList[i], 1, networkState.get((1, procIdList[i])).oneOf() + ) + ) ).then( // everyone computes a sequence number ComputeSeqNumber( From 96d708ce1b21d56f21040c425ca9dbc39a6461c9 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Wed, 25 Oct 2023 17:21:01 -0400 Subject: [PATCH 15/19] Start adding AssignSeqNumber --- genericMulticast/gmcast0.qnt | 37 +++++++++++++++++++++++++++++++++--- 1 file changed, 34 insertions(+), 3 deletions(-) diff --git a/genericMulticast/gmcast0.qnt b/genericMulticast/gmcast0.qnt index d92314e..fe72f26 100644 --- a/genericMulticast/gmcast0.qnt +++ b/genericMulticast/gmcast0.qnt @@ -40,7 +40,7 @@ module gmcast0 { var nodeState: ProcId -> NodeState var networkState: Network - pure def conflicts(lhs: Message, rhs: Message): bool = true + pure def conflicts(lhs: int, rhs: int): bool = true action init: bool = all { nodeState' = ProcIds.mapBy( @@ -153,13 +153,13 @@ module gmcast0 { ): (Network, NodeState) = { val newK = - if (noState.previous.exists(om => om.conflicts(m))) + if (noState.previous.exists(om => om.id.conflicts(m.id))) noState.k + 1 else noState.k val newPrevious = - if (noState.previous.exists(om => om.conflicts(m))) + if (noState.previous.exists(om => om.id.conflicts(m.id))) Set(m) else noState.previous.union(Set(m)) @@ -199,4 +199,35 @@ module gmcast0 { } } } + + action AssignSeqNumber(receiver: ProcId, id: int, sender: ProcId): bool = { + all { + // get the first message from sender to receiver with the id and + // tag S2 + val msg = networkState.get((sender, receiver)).fold( + // start with empty dummy message + {tag: "S2", timestamp: -1, dst: Set(), id: -1}, + (acc, m) => + if (m.id == id and m.tag == "S2") { + m + } else { + acc + } + ) + // get the node state of the receiver + val receiverState = nodeState.get(receiver) + // get the timestamp of the message + val tsf = msg.timestamp + // create the new node state + val newReceiverState = + { + k: receiverState.k, + pending: receiverState.pending.exclude(Set((msg, tsf))), + delivering: receiverState.delivering.union(Set(msg)), + delivered: receiverState.delivered, + previous: receiverState.previous + } + true + } + } } \ No newline at end of file From 9e9339bce268a057a664570272a49fef5cb87b4f Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Wed, 25 Oct 2023 17:46:30 -0400 Subject: [PATCH 16/19] Continue implementing AssignSeqNumber --- genericMulticast/gmcast0.qnt | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/genericMulticast/gmcast0.qnt b/genericMulticast/gmcast0.qnt index fe72f26..d10f1cf 100644 --- a/genericMulticast/gmcast0.qnt +++ b/genericMulticast/gmcast0.qnt @@ -218,15 +218,17 @@ module gmcast0 { val receiverState = nodeState.get(receiver) // get the timestamp of the message val tsf = msg.timestamp - // create the new node state - val newReceiverState = - { - k: receiverState.k, - pending: receiverState.pending.exclude(Set((msg, tsf))), - delivering: receiverState.delivering.union(Set(msg)), - delivered: receiverState.delivered, - previous: receiverState.previous - } + + // val newK = + // // create the new node state + // val newReceiverState = + // { + // k: if tsf > receiverState.k {k+1}, + // pending: receiverState.pending.exclude(Set((msg, tsf))), + // delivering: receiverState.delivering.union(Set(msg)), + // delivered: receiverState.delivered, + // previous: receiverState.previous + // } true } } From 8265af44909292bd80040d01536fc354bcbbc04c Mon Sep 17 00:00:00 2001 From: lasarojc Date: Wed, 25 Oct 2023 16:47:07 -0400 Subject: [PATCH 17/19] doDeliver skeleton --- genericMulticast/gmcast0.qnt | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/genericMulticast/gmcast0.qnt b/genericMulticast/gmcast0.qnt index d10f1cf..eefab29 100644 --- a/genericMulticast/gmcast0.qnt +++ b/genericMulticast/gmcast0.qnt @@ -231,5 +231,14 @@ module gmcast0 { // } true } + + + pure def DoDeliverHelper(): bool = { + true + } + + action DoDeliver(): bool = { + val newState = DoDeliverHelper + unchanged_all } } \ No newline at end of file From af42a4f73adb9ee80fbb58b961478d88359563f8 Mon Sep 17 00:00:00 2001 From: lasarojc Date: Thu, 26 Oct 2023 14:37:54 -0400 Subject: [PATCH 18/19] adding DoDeliver. Missing tests --- genericMulticast/gmcast0.qnt | 166 +++++++++++++++++++++-------------- 1 file changed, 99 insertions(+), 67 deletions(-) diff --git a/genericMulticast/gmcast0.qnt b/genericMulticast/gmcast0.qnt index eefab29..9f5e7b8 100644 --- a/genericMulticast/gmcast0.qnt +++ b/genericMulticast/gmcast0.qnt @@ -2,12 +2,17 @@ module gmcast0 { import spell.* from "./spell" type ProcId = int + pure val ProcIds = Set(1,2,3,4,5) + pure val Groups = Set( + Set(1,2), + Set(3,4), + Set(5) + ) //XXX Quint: Ideally these should be consts, but because it would have to be instantiated on every import, there would be duplication. //All processes in the system pure val MsgType = Set("S0", "S1", "S2") - pure val ProcIds = Set(1,2,3,4,5) type Message = { tag: str, //Shoud be in MsgType timestamp: int, // -1 means no timestamp @@ -18,18 +23,12 @@ module gmcast0 { type Channel = (ProcId, ProcId) - pure val Groups = Set( - Set(1,2), - Set(3,4), - Set(5) - ) - //Nodes keep the following state type NodeState = { k: int, pending: Set[(Message,int)], - delivering: Set[Message], - delivered: Set[Message], + delivering: Set[(Message,int)], + delivered: Set[(Message,int)], previous: Set[Message] } @@ -91,58 +90,6 @@ module gmcast0 { nodeState' = nodeState } } - - action ComputeSeqNumber(p: ProcId, id: int, dst: Set[Set[ProcId]]): bool = { - all { - // for all processes in dst, we have received an S1 - dst.flatten().forall( - receiver => - // there must be a message tagged with S1 sent by receiver to p relating to m - networkState.get((p, receiver)).exists( - msg => msg.id == id and - msg.tag == "S1" - ) - - ), - // get messages tagged with S1 received by p relating to the message id - val receivedMessages = dst.flatten().fold( - Set(), (acc, receiver) => - val msgsFromReceiver = networkState.get((receiver, p)).filter( - msg => msg.id == id and - msg.tag == "S1") - acc.union(msgsFromReceiver) - ) - - // find the maximal timestamp among the S1 messages - val timestamp_final = receivedMessages.fold( - -1, - (acc, msg) => - if (msg.timestamp > acc) { - msg.timestamp - } else { - acc - } - ) - // tag the message with S2 and the timestamp - val message_final = { - tag: "S2", - timestamp: timestamp_final, - dst: dst, - id: id - } - // send it to all destination processes - networkState' = - networkState.keys().mapBy( - channel => - if (dst.flatten().contains(channel._2)) { - networkState.get(channel).union(Set(message_final)) - } else { - networkState.get(channel) - } - ), - nodeState' = nodeState - } - } pure def AssignTimestampHelper( sender: ProcId, @@ -200,6 +147,58 @@ module gmcast0 { } } + action ComputeSeqNumber(p: ProcId, id: int, dst: Set[Set[ProcId]]): bool = { + all { + // for all processes in dst, we have received an S1 + dst.flatten().forall( + receiver => + // there must be a message tagged with S1 sent by receiver to p relating to m + networkState.get((p, receiver)).exists( + msg => msg.id == id and + msg.tag == "S1" + ) + + ), + // get messages tagged with S1 received by p relating to the message id + val receivedMessages = dst.flatten().fold( + Set(), (acc, receiver) => + val msgsFromReceiver = networkState.get((receiver, p)).filter( + msg => msg.id == id and + msg.tag == "S1") + acc.union(msgsFromReceiver) + ) + + // find the maximal timestamp among the S1 messages + val timestamp_final = receivedMessages.fold( + -1, + (acc, msg) => + if (msg.timestamp > acc) { + msg.timestamp + } else { + acc + } + ) + // tag the message with S2 and the timestamp + val message_final = { + tag: "S2", + timestamp: timestamp_final, + dst: dst, + id: id + } + // send it to all destination processes + networkState' = + networkState.keys().mapBy( + channel => + if (dst.flatten().contains(channel._2)) { + networkState.get(channel).union(Set(message_final)) + } else { + networkState.get(channel) + } + ), + nodeState' = nodeState + } + } + action AssignSeqNumber(receiver: ProcId, id: int, sender: ProcId): bool = { all { // get the first message from sender to receiver with the id and @@ -231,14 +230,47 @@ module gmcast0 { // } true } + } - - pure def DoDeliverHelper(): bool = { - true + pure def DoDeliverHelper( + p: ProcId, + ti: (Message, int), + noState: NodeState + ): NodeState = { + val mi = ti._1 + val tsi = ti._2 + val G = noState.delivering.filter(tj => + val mj = tj._1 + val tsj = tj._2 + noState.delivering + .union(noState.pending) + .exclude(Set(tj)) + .forall(tk => + val mk = tk._1 + val tsk = tk._2 + not(mj.id.conflicts(mk.id)) + ) + ) + val D = Set(ti).union(G) + val newNoState = { + delivering: noState.delivering.exclude(D), + delivered: noState.delivered.union(D), + ...noState + } + + /* The following lines is in the algorithm but has not been specified. + val msgsToDeliver = D.map(e => e._1) + msgsToDeliver.forall(m, GMDeliver(m)) + */ + newNoState } - action DoDeliver(): bool = { - val newState = DoDeliverHelper - unchanged_all + action DoDeliver(p: ProcId): bool = { + val mi = ({tag: "S1", timestamp: -1, dst: Groups, id:1}, 3) + val newNodeState = DoDeliverHelper(p, mi, nodeState.get(p)) + all { + nodeState' = nodeState.set(p, newNodeState), + networkState' = networkState + } } } \ No newline at end of file From 2dc710e8a1da0757e795b20174463ee34ace982c Mon Sep 17 00:00:00 2001 From: hvanz Date: Thu, 26 Oct 2023 18:17:19 -0400 Subject: [PATCH 19/19] AssignSeqNumber --- genericMulticast/gmcast0.qnt | 53 ++++++++++++++++-------------------- genericMulticast/spell.qnt | 33 ++++++++++++++++++++++ genericMulticast/tests.qnt | 10 +++++++ 3 files changed, 66 insertions(+), 30 deletions(-) diff --git a/genericMulticast/gmcast0.qnt b/genericMulticast/gmcast0.qnt index 9f5e7b8..dfd3c7c 100644 --- a/genericMulticast/gmcast0.qnt +++ b/genericMulticast/gmcast0.qnt @@ -199,39 +199,32 @@ module gmcast0 { } } - action AssignSeqNumber(receiver: ProcId, id: int, sender: ProcId): bool = { - all { - // get the first message from sender to receiver with the id and - // tag S2 - val msg = networkState.get((sender, receiver)).fold( - // start with empty dummy message - {tag: "S2", timestamp: -1, dst: Set(), id: -1}, - (acc, m) => - if (m.id == id and m.tag == "S2") { - m - } else { - acc - } - ) - // get the node state of the receiver - val receiverState = nodeState.get(receiver) - // get the timestamp of the message - val tsf = msg.timestamp - - // val newK = - // // create the new node state - // val newReceiverState = - // { - // k: if tsf > receiverState.k {k+1}, - // pending: receiverState.pending.exclude(Set((msg, tsf))), - // delivering: receiverState.delivering.union(Set(msg)), - // delivered: receiverState.delivered, - // previous: receiverState.previous - // } - true + + def AssignSeqNumberState(msg: Message, state: NodeState): NodeState = + val newState = { ...state, + pending: state.pending.exclude(Set((msg, msg.timestamp))), + delivering: state.delivering.union(Set((msg, msg.timestamp))) } + if (msg.timestamp > state.k) { + if (state.previous.exists(m => m == msg)) + { ...newState, k: msg.timestamp + 1, previous: Set() } + else + { ...newState, k: msg.timestamp } + } else newState + + action AssignSeqNumberFor(sender: ProcId, receiver: ProcId, msg: Message): bool = all { + nodeState' = nodeState.mapPut(receiver, state => AssignSeqNumberState(msg, state)), + networkState' = networkState.mapPut((sender, receiver), msgs => msgs.exclude(Set(msg))) } + action AssignSeqNumber(sender: ProcId, receiver: ProcId): bool = + val msgs = networkState.get((sender, receiver)).filter(m => m.tag == "S2") + all { + require(msgs.nonEmpty()), + nondet msg = oneOf(msgs) + AssignSeqNumberFor(sender, receiver, msg) + } + pure def DoDeliverHelper( p: ProcId, ti: (Message, int), diff --git a/genericMulticast/spell.qnt b/genericMulticast/spell.qnt index 5f8ba45..e3c4081 100644 --- a/genericMulticast/spell.qnt +++ b/genericMulticast/spell.qnt @@ -15,4 +15,37 @@ module spell { crossproduct(Set(), Set()) == Set(), } } + + //-------------------------------------------------------------------------- + /// An annotation for writing preconditions. + pure def require(__cond: bool): bool = __cond + + /// Remove a set element. + pure def setRemove(__set: Set[a], __elem: a): Set[a] = { + __set.exclude(Set(__elem)) + } + + /// Remove a map entry. + pure def mapRemove(__map: a -> b, __key: a): a -> b = { + __map.keys().setRemove(__key).mapBy(__k => __map.get(__k)) + } + + //-------------------------------------------------------------------------- + pure def isEmpty(__set: Set[a]): bool = + __set == Set() + + pure def nonEmpty(__set: Set[a]): bool = + __set != Set() + + //-------------------------------------------------------------------------- + /// Update a map entry using the previous value. + /// + /// @param __map the map to update + /// @param __key the key to search for + /// @param __f a function that returns the new value for __key + /// when applied to __key's old value + /// @returns a new map equal to __map except that __key maps + /// to __f applied to __key's old value + pure def mapPut(__map: a -> b, __key: a, __f: b => b): (a -> b) = + __map.put(__key, __f(__map.get(__key))) } \ No newline at end of file diff --git a/genericMulticast/tests.qnt b/genericMulticast/tests.qnt index 80fd6f8..d3f9e52 100644 --- a/genericMulticast/tests.qnt +++ b/genericMulticast/tests.qnt @@ -70,4 +70,14 @@ module tests { ) ) } + + // auxiliary action for assertions + action _assert(pred: bool): bool = all { assert(pred), unchanged_all } + + run AssignSeqNumberTest = + ComputeSeqNumberTest + .then(_assert(nodeState.get(2).k == 0)) + .then(AssignSeqNumberFor(1, 2, { tag: "S2", timestamp: 5, dst: Set(Set()), id: 1 })) + .then(_assert(nodeState.get(2).k == 5)) + }