1
00:00:04,280 --> 00:00:07,920
>> Hello, my name is Heba and
I'm presenting an extension

2
00:00:07,920 --> 00:00:11,415
of PlusCal for Modeling
Distributed Algorithms.

3
00:00:11,415 --> 00:00:15,015
Lets start out by
saying what is TLA_+?

4
00:00:15,015 --> 00:00:17,715
TLA_+ is a formal
specification language.

5
00:00:17,715 --> 00:00:22,630
It is mainly used to model concurrent
and distributed algorithms.

6
00:00:22,630 --> 00:00:26,790
The TLA_+ Toolbox is an ID
that provides many tools such

7
00:00:26,790 --> 00:00:31,725
as a model checker and an interactive
hoof assistant for example.

8
00:00:31,725 --> 00:00:34,500
Since TLA_+ is more of

9
00:00:34,500 --> 00:00:37,874
a specification formalism rather
than a programming language,

10
00:00:37,874 --> 00:00:41,610
it can be challenging for
programmers to use it initially.

11
00:00:41,610 --> 00:00:44,240
PlusCal is an algorithmic
language that was

12
00:00:44,240 --> 00:00:47,690
created to accompany TLA_+ to give

13
00:00:47,690 --> 00:00:50,720
the users more of a
familiar syntax while

14
00:00:50,720 --> 00:00:55,110
maintaining the same
expressiveness as TLA_+.

15
00:00:56,050 --> 00:01:01,630
However, if we're discussing
distributed algorithms,

16
00:01:01,630 --> 00:01:05,869
we usually find ourselves needing
to model a directive processes

17
00:01:05,869 --> 00:01:10,250
that into play together in order
to carry out a certain task.

18
00:01:10,250 --> 00:01:14,550
This need is not really
met naturally in PlusCal

19
00:01:14,550 --> 00:01:17,030
since PlusCal has more flat hierarchy

20
00:01:17,030 --> 00:01:18,864
when it comes to its processes,

21
00:01:18,864 --> 00:01:22,340
and it doesn't really allow
annesting of processes.

22
00:01:22,340 --> 00:01:25,560
We propose an extension
of PlusCal called

23
00:01:25,560 --> 00:01:30,460
distributed PlusCal that
enables the users to define

24
00:01:30,460 --> 00:01:35,200
sub-processes to model this
parallelism as well as providing

25
00:01:35,200 --> 00:01:38,050
communication channel
constructs that can help in

26
00:01:38,050 --> 00:01:41,990
the communication between
these sub-processes.

27
00:01:42,350 --> 00:01:45,490
We're going to start
out by introducing

28
00:01:45,490 --> 00:01:48,895
motivational example to
highlight all contributions.

29
00:01:48,895 --> 00:01:51,655
We have chosen Lamport's
Mutex Algorithm.

30
00:01:51,655 --> 00:01:53,230
For those of you who are not aware,

31
00:01:53,230 --> 00:01:55,570
it's an algorithm for
mutual exclusion and

32
00:01:55,570 --> 00:01:59,500
distributed systems where
processes request access to

33
00:01:59,500 --> 00:02:02,485
a critical section
and each request has

34
00:02:02,485 --> 00:02:04,570
a logical clock value where

35
00:02:04,570 --> 00:02:08,185
the requests with the lower
values have higher priority.

36
00:02:08,185 --> 00:02:12,800
A process starts out by sending a
request that it needs to access

37
00:02:12,800 --> 00:02:15,034
the critical section to
all the other processes

38
00:02:15,034 --> 00:02:18,600
with a logical clock value.

39
00:02:18,600 --> 00:02:21,245
Then it waits for the
acknowledgment from

40
00:02:21,245 --> 00:02:23,150
all the other processes to give

41
00:02:23,150 --> 00:02:25,600
it a right to enter
the critical section.

42
00:02:25,600 --> 00:02:27,940
Once all the acknowledgements
are received,

43
00:02:27,940 --> 00:02:30,800
it enters the critical
section, execute its part,

44
00:02:30,800 --> 00:02:33,545
and then when it leaves
the critical section,

45
00:02:33,545 --> 00:02:35,510
it notifies all the other processes

46
00:02:35,510 --> 00:02:39,190
that the critical
section is now released.

47
00:02:39,250 --> 00:02:43,050
If we're going to model
this algorithm in PlusCal,

48
00:02:43,050 --> 00:02:44,955
we're going to need
two process types.

49
00:02:44,955 --> 00:02:46,490
The first process type will be

50
00:02:46,490 --> 00:02:49,535
just a process to carry
out the main algorithm.

51
00:02:49,535 --> 00:02:51,080
We can see here that we have

52
00:02:51,080 --> 00:02:53,685
a non-critical section
and then you have

53
00:02:53,685 --> 00:02:55,940
a trystep where you
multicast the message

54
00:02:55,940 --> 00:02:58,820
requesting the access to
the critical section.

55
00:02:58,820 --> 00:03:00,800
Then in the following step,

56
00:03:00,800 --> 00:03:03,985
you wait for the acknowledgments
from all the other processes.

57
00:03:03,985 --> 00:03:06,290
Once you get all your
acknowledgements,

58
00:03:06,290 --> 00:03:09,620
you can move forward and
enter the critical section.

59
00:03:09,620 --> 00:03:11,600
Eventually when you exit,

60
00:03:11,600 --> 00:03:15,080
you again multicast a
release message for

61
00:03:15,080 --> 00:03:16,985
all the processes notifying them

62
00:03:16,985 --> 00:03:20,040
that the critical
section is now released.

63
00:03:20,770 --> 00:03:25,140
We also need a helper process
that can be responsible for

64
00:03:25,140 --> 00:03:30,190
the communication
between the processes.

65
00:03:30,190 --> 00:03:32,530
The helper process here

66
00:03:32,530 --> 00:03:35,840
uses an operator that we
have defined called node.

67
00:03:35,840 --> 00:03:38,750
Node here identifies the main process

68
00:03:38,750 --> 00:03:42,830
corresponding to the communicator
C. Inside this block here,

69
00:03:42,830 --> 00:03:46,370
we're handling requested
knowledge and released messages.

70
00:03:46,370 --> 00:03:49,895
Because we have two
processes working together,

71
00:03:49,895 --> 00:03:52,970
the variables must be
declared globally in

72
00:03:52,970 --> 00:03:57,060
order for them to be
accessible by both processes.

73
00:03:57,320 --> 00:04:00,290
However, if we decide

74
00:04:00,290 --> 00:04:03,410
to model this algorithm
in distributed PlusCal,

75
00:04:03,410 --> 00:04:06,290
it can be done in a simpler way.

76
00:04:06,290 --> 00:04:10,545
For example, we will have only
one process type where you have

77
00:04:10,545 --> 00:04:15,005
two sub-processes working together
to carry out this algorithms.

78
00:04:15,005 --> 00:04:17,300
The first sub-process starts with

79
00:04:17,300 --> 00:04:21,075
this curly brace here and ends
with this curly brace here.

80
00:04:21,075 --> 00:04:22,620
Same thing for the second one,

81
00:04:22,620 --> 00:04:24,455
it starts here and ends here,

82
00:04:24,455 --> 00:04:26,855
where the first
sub-process carries out

83
00:04:26,855 --> 00:04:29,750
the same logic that we
have discussed before you

84
00:04:29,750 --> 00:04:31,985
have an uncritical
section and all the way

85
00:04:31,985 --> 00:04:34,895
to releasing the critical section and

86
00:04:34,895 --> 00:04:41,610
the second sub-process handles the
asynchronous message reception.

87
00:04:41,750 --> 00:04:45,920
As for modeling channels for
this specific algorithm,

88
00:04:45,920 --> 00:04:49,135
in PlusCal we declare
a variable here.

89
00:04:49,135 --> 00:04:52,510
We give it two dimensions where p
can be the sender of a message,

90
00:04:52,510 --> 00:04:54,860
q can be the receiver
and the messages are

91
00:04:54,860 --> 00:04:58,010
placed within the TNA_+ sequence.

92
00:04:58,010 --> 00:05:00,200
In distributed PlusCal however,

93
00:05:00,200 --> 00:05:03,370
you can simply declare a
predefined type called FIFOs to

94
00:05:03,370 --> 00:05:07,745
represent a FIFO channel and give
it the appropriate dimensions.

95
00:05:07,745 --> 00:05:10,430
Also for implementing an operation

96
00:05:10,430 --> 00:05:12,350
in PlusCal, a channel operation,

97
00:05:12,350 --> 00:05:13,640
you will define a macro,

98
00:05:13,640 --> 00:05:15,380
give it the appropriate body,

99
00:05:15,380 --> 00:05:18,295
and then later on call the macro.

100
00:05:18,295 --> 00:05:21,185
Where in distributed PlusCal you can

101
00:05:21,185 --> 00:05:23,675
simply use one of the
predefined operators.

102
00:05:23,675 --> 00:05:26,000
For example here we
have an operator called

103
00:05:26,000 --> 00:05:30,395
multicast where the first argument
represents the channel name

104
00:05:30,395 --> 00:05:33,875
and the second argument
represents an expression that

105
00:05:33,875 --> 00:05:35,930
specifies the intended recipients

106
00:05:35,930 --> 00:05:39,240
as well as the message
that needs to be sent.

107
00:05:39,850 --> 00:05:42,710
Here we can see the general structure

108
00:05:42,710 --> 00:05:45,500
of a distributed PlusCal Algorithm.

109
00:05:45,500 --> 00:05:49,460
It resembles the general
structure of a PlusCal Algorithm.

110
00:05:49,460 --> 00:05:51,860
The differences can be
seen here where you can

111
00:05:51,860 --> 00:05:56,180
define channels to represent
unordered channels.

112
00:05:56,180 --> 00:06:00,260
You can define FIFO's like
we have seen in our example.

113
00:06:00,260 --> 00:06:03,920
Here, instead of giving
the process one body,

114
00:06:03,920 --> 00:06:07,260
you can actually give it
multiple sub-processes.

115
00:06:07,640 --> 00:06:11,130
We have supported several
operations on channels.

116
00:06:11,130 --> 00:06:14,690
For example, you can send a
single element to a channel,

117
00:06:14,690 --> 00:06:18,785
you can receive as enabled
when an empty channel receives

118
00:06:18,785 --> 00:06:20,905
a message into a variable

119
00:06:20,905 --> 00:06:23,510
as can be seen here in
the second argument.

120
00:06:23,510 --> 00:06:26,525
Broadcast and multicast
send messages along

121
00:06:26,525 --> 00:06:31,895
several channels in an array
while clear empties the channel.

122
00:06:31,895 --> 00:06:34,940
If we take a look at
unordered channels,

123
00:06:34,940 --> 00:06:36,455
we will see that they are declared

124
00:06:36,455 --> 00:06:39,485
using the keyword
channel or channels.

125
00:06:39,485 --> 00:06:43,055
They are also based on TNA_+ sets.

126
00:06:43,055 --> 00:06:46,010
If a channel operation is actually

127
00:06:46,010 --> 00:06:48,470
invoked with an ordered channel,

128
00:06:48,470 --> 00:06:51,170
once it is translated to TLA_+,

129
00:06:51,170 --> 00:06:54,650
it will be using the
TLA _+ set operators,

130
00:06:54,650 --> 00:06:58,270
as we can see here and here as well.

131
00:06:58,270 --> 00:07:00,740
As for FIFO channels,

132
00:07:00,740 --> 00:07:01,970
they are declared using

133
00:07:01,970 --> 00:07:04,805
the keyword FIFO as we
have seen in our example,

134
00:07:04,805 --> 00:07:08,360
and they are based on TLA_+
sequences because we want to

135
00:07:08,360 --> 00:07:13,570
maintain the order between the
messages within the channel itself.

136
00:07:13,570 --> 00:07:18,080
Once an operator is
translated into TLA_+,

137
00:07:18,080 --> 00:07:20,975
it will be using the
TLA_+ sequence operators

138
00:07:20,975 --> 00:07:24,780
such as append, head, and tail.

139
00:07:25,790 --> 00:07:28,080
As for the variable,

140
00:07:28,080 --> 00:07:31,485
it is a special variable
TLA_+ and PlusCal.

141
00:07:31,485 --> 00:07:34,040
It should present a
single string equal to

142
00:07:34,040 --> 00:07:36,185
the label of this next statement

143
00:07:36,185 --> 00:07:38,420
to be executed with
respect to a process.

144
00:07:38,420 --> 00:07:41,300
We have extended this definition to

145
00:07:41,300 --> 00:07:45,960
include which sub-process
is involved as well.

146
00:07:45,960 --> 00:07:51,420
Here we can see the initialization
of the pc variable.

147
00:07:51,420 --> 00:07:56,615
For example, if we are
handling a process of type p1,

148
00:07:56,615 --> 00:07:59,255
here we'll be giving a sequence where

149
00:07:59,255 --> 00:08:03,370
lbl_11 represents the first
label in the first sub-process,

150
00:08:03,370 --> 00:08:06,200
and lbl_12 will represent

151
00:08:06,200 --> 00:08:10,205
the first label in the second
sub-process and so on.

152
00:08:10,205 --> 00:08:12,980
Here is a piece of translation

153
00:08:12,980 --> 00:08:15,110
that was produced by
our own translator.

154
00:08:15,110 --> 00:08:17,810
This is the same exit
all set that we have

155
00:08:17,810 --> 00:08:20,734
discussed before when
the process exits

156
00:08:20,734 --> 00:08:23,840
the critical section and
it releases a message for

157
00:08:23,840 --> 00:08:26,060
all the other processes
notifying them that

158
00:08:26,060 --> 00:08:29,755
the critical section is now released.

159
00:08:29,755 --> 00:08:32,730
The first thing to pay

160
00:08:32,730 --> 00:08:35,555
attention to is the fact
that the pc variable,

161
00:08:35,555 --> 00:08:38,285
it also references the number 1 here,

162
00:08:38,285 --> 00:08:42,290
which means that we are
in the first sub-process.

163
00:08:42,290 --> 00:08:45,710
These lines represent
the translation of

164
00:08:45,710 --> 00:08:49,990
a multicasts operation when
invoked with a FIFO channel.

165
00:08:49,990 --> 00:08:53,540
We can see here even
the PC prime variable

166
00:08:53,540 --> 00:08:58,340
also takes into consideration
in which sub-process we are.

167
00:08:58,340 --> 00:09:00,650
Though to conclude, we offer

168
00:09:00,650 --> 00:09:03,575
an extension of PlusCal
called distributed PlusCal.

169
00:09:03,575 --> 00:09:06,200
It gives the user the
opportunity to define

170
00:09:06,200 --> 00:09:08,345
sub-processes that you would normally

171
00:09:08,345 --> 00:09:10,820
see coexisting within
a distributed node.

172
00:09:10,820 --> 00:09:13,960
We also offer a communication
channel constructs

173
00:09:13,960 --> 00:09:19,250
that assists in the communication
between these subprocesses.

174
00:09:19,250 --> 00:09:21,799
We offer backward-compatible
translator

175
00:09:21,799 --> 00:09:23,570
that translates from PlusCal

176
00:09:23,570 --> 00:09:27,895
to TLA_+ as well as from
distributed PlusCal to TLA_+.

177
00:09:27,895 --> 00:09:32,750
This is because we used the
same translator that exists

178
00:09:32,750 --> 00:09:38,540
within the TLA_+ Toolbox before
we extended the language.

179
00:09:38,540 --> 00:09:41,120
For future work, we intend to

180
00:09:41,120 --> 00:09:43,310
introduce more types of
communication channels.

181
00:09:43,310 --> 00:09:46,130
We are also considering defining

182
00:09:46,130 --> 00:09:49,205
TLA_+ standard module that

183
00:09:49,205 --> 00:09:52,475
the channel operations can
get their definitions from.

184
00:09:52,475 --> 00:09:56,540
This can give the user far much
more flexibility to define

185
00:09:56,540 --> 00:09:58,880
their own operations as well as

186
00:09:58,880 --> 00:10:02,225
override the operations they
have already introduced.

187
00:10:02,225 --> 00:10:06,515
Thank you so much for watching
and feel free to take a look at

188
00:10:06,515 --> 00:10:12,000
our GitHub repository and try
out our translator. Thanks.