Two Phase Commit (Actor model/Object oriented)
This is another implementation style in FizzBee to model the Two Phase Commit protocol. There are two other styles,
- Functional style similar to TLA+
- Procedural style similar to PlusCal
- Object oriented style (this post) similar to P
The significant benefit of this style is, it would feel more natural to the actual implementation, but at the same higher level of abstraction as the other styles but more concise than the other options.
For more information about Roles, refer to Roles.
For the details on the algorithm read through the previous posts.
One way to think of it is, this is just a syntactic sugar over the procedural styles.
This document assumes, you are already familar with the procedural style. Just go through the Two Phase Commit (Procedural) doc to get a quick overview.
Two major new concepts used here are
- Roles
- Channels
Roles are like classes in object oriented programming. They have states and actions. But here, they may represent a participant in a system. It could be a,
- microservice
- process
- thread
- just a role (Eg. coordinator, participant in 2-Phase Commit)
- database
If you are writing a design doc, and created a block diagram with it, they most likely represent a role in the system.
Roles can have state, actions, functions and even assertions like a top level spec. So basically, roles just provide a way to organize the code.
role Server1:
action Init(args):
# ...
action OtherAction:
# ...
The communication mechanism to connect two roles. This simplifies modeling of message passing.
- Blocking/NonBlocking - default=blocking
- Delivery (at most once, at least once, exactly once) - default = “atmost_once”
- Ordering (unordered, pairwise, ordered) - ordering = “unordered”
Unlike the P model checker that has separate send semantics and new method, to use the channels there is no syntax change. Just call the other function like a normal function call.
As you saw in the previous example, message passing is just a function call. To make it even easier, the default channels are defined that you would never need to deal with these in most cases.
By default,
- For intra role communication,
- Blocking, exactly once, unordered
- For inter role communication,
- Blocking, at most once, unordered
In the procedural approach, we had 3 state variables, tmState, rmState, tmPrepared.
As the names indicate, rmState corresponds to the states of each participant.
It’s key and value, will become the state variables for each participant.
Similarly, RmPrepare, RmAbort and RmCommit will become the functions for each participant.
At this point, the syntax should be familiar.
role Participant:
action Init:
self.state = "working"
fair action Timeout:
if self.state == "working":
self.state = "aborted"
func Prepare():
if self.state != 'working':
return self.state
oneof:
self.state = 'prepared'
self.state = 'aborted'
return self.state
func Commit():
self.state = 'committed'
func Abort():
self.state = 'aborted'
action Terminated:
if self.state == 'committed':
pass
Coordinator has state and list of prepared participants.
role Coordinator:
action Init:
self.prepared = set()
self.state = "init"
action Write:
if self.state != "init":
return
self.state = "working"
for p in participants:
vote = p.Prepare()
if vote == 'aborted':
self.Abort()
return
self.prepared.add(p.ID)
self.Commit()
fair action Timeout:
if self.state != "committed":
self.Abort()
fair action Restart:
if self.state == "committed":
for p in participants:
p.Commit()
func Abort():
self.state = "aborted"
for p in participants:
p.Abort()
func Commit():
if self.state == 'working' and len(self.prepared) == len(participants):
self.state = 'committed'
for p in participants:
p.Commit()
Now, we just need a way to instantiate the roles and connect them.
action Init:
participants = []
for i in range(NUM_PARTICIPANTS):
p = Participant(ID=i)
participants.append(p)
coordinator = Coordinator()
Although the invariants can be specified within the roles, it is easier to verify the system level properties at the top level. Especially, when the properties are not specific to a role like in the case of two phase commit. We need a way to accesss the states of all participants.
In our case, we can put that in the global part itself.
always assertion ResMgrsConsistent:
for p1 in participants:
for p2 in participants:
if p1.state == 'committed' and p2.state == 'aborted':
return False
return True
eventually always assertion Terminated:
return coordinator.state in ('committed', 'aborted')
|
|
Click on the Communication Diagram link to see the communication diagram.
This shows the various roles and the messages exchanged between them.
This is a more detailed diagram. To generate this, first enable whiteboard and then run.
You will see Explorer link, click to open it.
On the left, play with the buttons to generate the sequence diagram.
sequenceDiagram
note left of 'Coordinator#0': Write
'Coordinator#0' ->> 'Participant#0': Prepare()
'Participant#0' -->> 'Coordinator#0': ("prepared")
'Coordinator#0' ->> 'Participant#1': Prepare()
'Participant#1' -->> 'Coordinator#0': ("prepared")
'Coordinator#0' ->> 'Participant#0': Commit()
'Participant#0' -->> 'Coordinator#0': .
'Coordinator#0' ->> 'Participant#1': Commit()
'Participant#1' -->> 'Coordinator#0': .
Compare this with the P model checker code.
https://github.com/p-org/P/tree/master/Tutorial/2_TwoPhaseCommit/PSrc
If you notice, the FizzBee code is more concise and closer to pseudocode. In addition to being concise, FizzBee does exhaustive model checking. Whereas, P does not. It explores various paths heuristically. That means, P cannot verify the correctness of the system, but FizzBee can.
This TLA+ example is written by Leslie Lamport in TLA+: https://github.com/tlaplus/Examples/blob/master/specifications/transaction_commit/TwoPhase.tla
Take a look at the readability of the FizzBee spec vs the TLA+ spec, making FizzBee a viable alternative to TLA+ and the easiest formal methods language so far.
I couldn’t find a pure PlusCal implementation, but a slightly modified version https://github.com/muratdem/PlusCal-examples/blob/master/2PCTM/2PCwithBTM.tla
Note: This post shows the Actor/Object oriented style of implementation.
FizzBee is a multi-paradigm language, so you can use the style that suits you best.