Lift the declarative history definition to the library

This commit is contained in:
Smaug123
2022-10-27 21:53:01 +01:00
parent 3c40471d7e
commit cce92eb9fd
4 changed files with 100 additions and 63 deletions

View File

@@ -70,12 +70,6 @@ module Program =
printf "Unrecognised input. "
None
type UserAction =
| InactivityTimeout of int<ServerId>
| NetworkMessage of int<ServerId> * int
| DropMessage of int<ServerId> * int
| Heartbeat of int<ServerId>
let rec getAction (clusterSize : int) =
printf
"Enter action. Trigger [t]imeout <server id>, [h]eartbeat a leader <server id>, [d]rop message <server id, message id>, or allow [m]essage <server id, message id>: "
@@ -108,15 +102,17 @@ module Program =
printf "Unrecognised input. "
getAction clusterSize
let processAction (cluster : Cluster<'a>) (network : Network<'a>) (action : UserAction) : unit =
match action with
| InactivityTimeout serverId -> cluster.InactivityTimeout serverId
| Heartbeat serverId -> cluster.HeartbeatTimeout serverId
| DropMessage (serverId, messageId) -> network.DropMessage serverId messageId
| NetworkMessage (serverId, messageId) ->
network.InboundMessage serverId messageId |> cluster.SendMessage serverId
network.DropMessage serverId messageId
let electLeader =
[
NetworkAction.InactivityTimeout 0<ServerId>
NetworkAction.NetworkMessage (1<ServerId>, 0)
NetworkAction.NetworkMessage (2<ServerId>, 0)
NetworkAction.DropMessage (3<ServerId>, 0)
NetworkAction.DropMessage (4<ServerId>, 0)
NetworkAction.NetworkMessage (0<ServerId>, 0)
NetworkAction.NetworkMessage (0<ServerId>, 1)
// At this point, server 0 is leader in an uncontested election.
]
[<EntryPoint>]
let main _argv =
@@ -125,24 +121,45 @@ module Program =
let startupSequence =
[
UserAction.InactivityTimeout 0<ServerId>
UserAction.NetworkMessage (1<ServerId>, 0)
UserAction.NetworkMessage (2<ServerId>, 0)
UserAction.DropMessage (3<ServerId>, 0)
UserAction.DropMessage (4<ServerId>, 0)
UserAction.NetworkMessage (0<ServerId>, 0)
UserAction.NetworkMessage (0<ServerId>, 1)
NetworkAction.InactivityTimeout 0<ServerId>
NetworkAction.InactivityTimeout 1<ServerId>
// Two servers vote for server 1...
NetworkAction.NetworkMessage (2<ServerId>, 1)
NetworkAction.NetworkMessage (3<ServerId>, 1)
// One server votes for server 0...
NetworkAction.NetworkMessage (4<ServerId>, 0)
// and the other votes are processed and discarded
NetworkAction.NetworkMessage (0<ServerId>, 0)
NetworkAction.NetworkMessage (1<ServerId>, 0)
NetworkAction.NetworkMessage (2<ServerId>, 0)
NetworkAction.NetworkMessage (3<ServerId>, 0)
NetworkAction.NetworkMessage (4<ServerId>, 1)
// Server 0 process incoming votes
NetworkAction.NetworkMessage (0<ServerId>, 1)
// Server 1 processes incoming votes, and achieves majority, electing itself leader!
NetworkAction.NetworkMessage (1<ServerId>, 1)
NetworkAction.NetworkMessage (1<ServerId>, 2)
// Get the followers' heartbeat processing out of the way
NetworkAction.NetworkMessage (2<ServerId>, 2)
NetworkAction.NetworkMessage (3<ServerId>, 2)
NetworkAction.NetworkMessage (4<ServerId>, 2)
NetworkAction.NetworkMessage (1<ServerId>, 3)
NetworkAction.NetworkMessage (1<ServerId>, 4)
NetworkAction.NetworkMessage (1<ServerId>, 5)
// Server 0 processes the leader's heartbeat and drops out of the election.
NetworkAction.NetworkMessage (0<ServerId>, 2)
NetworkAction.NetworkMessage (1<ServerId>, 6)
]
for action in startupSequence do
processAction cluster network action
NetworkAction.perform cluster network action
while true do
printNetworkState network
printClusterState cluster
let action = getAction clusterSize
processAction cluster network action
NetworkAction.perform cluster network action
// TODO: log out the committed state so that we can see whether the leader is correctly
// processing heartbeat responses