FizzBee
GitHub Toggle Dark/Light/Auto mode Toggle Dark/Light/Auto mode Toggle Dark/Light/Auto mode Back to homepage

Two Phase Commit (Actor model/Object oriented)

Two Phase Commit (Object oriented/Actor style implementation)

This is another implementation style in FizzBee to model the Two Phase Commit protocol. There are two other styles,

  1. Functional style similar to TLA+
  2. Procedural style similar to PlusCal
  3. 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.

Quick overview

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

  1. Roles
  2. Channels

Roles

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:
    # ...

Channels

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

Implementation

Roles - Participants

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

Role - Coordinator

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()

Driver program

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)

Safety invariant

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

Liveness invariant

eventually always assertion Terminated:
  return coordinator.state in ('committed', 'aborted')

Complete code

Run in playground
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
NUM_PARTICIPANTS = 2

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()


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'

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')


action Init:
  participants = []
  for i in range(NUM_PARTICIPANTS):
    p = Participant(ID=i)
    participants.append(p)

  coordinator = Coordinator(PARTICIPANTS=participants)

Diagrams

Communication Diagram

Click on the Communication Diagram link to see the communication diagram. This shows the various roles and the messages exchanged between them.

Interactive Sequence Diagram

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': .
   

Whiteboard diagram

Compare with P

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.