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 rm in self.PARTICIPANTS:
vote = rm.Prepare()
if vote == 'aborted':
self.Abort()
return
self.prepared.add(rm.ID)
self.Commit()
fair action Timeout:
if self.state != "committed":
self.Abort()
fair action Restart:
if self.state == "committed":
for rm in self.PARTICIPANTS:
rm.Commit()
func Abort():
self.state = "aborted"
for rm in self.PARTICIPANTS:
rm.Abort()
func Commit():
if self.state == 'working' and len(self.prepared) == len(self.PARTICIPANTS):
self.state = 'committed'
for rm in self.PARTICIPANTS:
rm.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(PARTICIPANTS=participants)
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 rm1 in participants:
for rm2 in participants:
if rm1.state == 'committed' and rm2.state == 'aborted':
return False
return True
eventually always assertion Terminated:
return coordinator.state in ('committed', 'aborted')
|
|
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.
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.