Skip to content

Commit

Permalink
added the examples rsts
Browse files Browse the repository at this point in the history
  • Loading branch information
@reututy
reututy committed May 3, 2018
1 parent 620eab4 commit 10a2a33
Show file tree
Hide file tree
Showing 5 changed files with 491 additions and 1 deletion.
200 changes: 200 additions & 0 deletions docs/source/example-TTT.rst
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,200 @@
Example - Tic Tac Toe

This example is borrowed, with modifications, from [10]. Its main feature is that it presents the concept of aligning bthreads to requirements. Meaning, each b-thread represents a rule, or a part of the tactics in the game of Tic-Tac-Toe.
First, let us describe the (classical) game of Tic-Tac-Toe, and the events that represent the expected behaviors. Two players, X and O, alternately mark squares on a 3 _ 3 grid whose squares are identified by (row; column) pairs: (0; 0); (0; 1); : : : ; (2; 2). The winner is the player who manages to form a full horizontal, vertical, or diagonal line with three of his/her marks. If the entire grid becomes marked but no player has formed a line, the result is a draw. Below, we assume player X is played by a human user, and player O is played by the application.
The goal of the programmer here is to implement the tactics for the O player such that the computer never loses. To check this main requirement, we use our model-checking tool that we will present soon. The game rules translate into b-threads as follows:

1 bp.registerBThread("EnforceTurns", function() {
2 while (true) {
3 bsync({waitFor:[X(0,0),X(0,1),...,X(2,2)],
4 block:[O(0,0),O(0,1),...,O(2,2)]});
5
6 bsync({waitFor:[O(0,0),O(0,1),...,O(2,2)],
7 block:[X(0,0),X(0,1),...,X(2,2)]});
8 }
9 });
Listing 13. A b-thread that implements the requirement that X and O play
alternatively.
1 bp.registerBThread("SqrTkn("+row+","+col+")",
function(){
2 while (true) {
3 bsync({waitFor:[X(row,col), O(row,col)]});
4 bsync({block:[X(row,col), O(row,col)]});
5 }
6 });
Listing 14. A b-thread that implements the requirement that a square may
only be marked once. Given the variables row and col that represent the
coordinates of a square on the grid, the b-thread waits for a move on that
square and blocks further moves on the same square.
1 var move = bp.EventSet("Mvs", e=>e instanceof Move);
2 bp.registerBThread("DetectDraw", function() {
3 for (var i=0; i<9; i++) {
4 bsync({waitFor:[move]});
5 }
6 bsync({request:[draw]}, 90);
7 });
Listing 15. A b-thread that implements the draw ending condition. It waits
for nine moves and then requests to announce a draw. The variable move
is a representation of all events of type Move. The number 90 specifies the
priority of the request.
1 bp.registerBThread("DetectXWin", function() {
2 while (true) {
3 bsync({waitFor:[X(l[p[0]].x, l[p[0]].y)]});
4 bsync({waitFor:[X(l[p[1]].x, l[p[1]].y)]});
5 bsync({waitFor:[X(l[p[2]].x, l[p[2]].y)]});
6 bsync({request:[XWin]}, 100);
7 }
8 });
Listing 16. A b-thread that implements the X winning condition. Given a
permutation p and a line l (row, column, or diagonal), the b-thread waits for
three X events on the line, in the order specified by the permutation, and then
requests to announce that X wins the game.
1 bp.registerBThread("DetectOWin", function() {
2 while (true) {
3 bsync({waitFor:[O(l[p[0]].x, l[p[0]].y)]});
4 bsync({waitFor:[O(l[p[1]].x, l[p[1]].y)]});
5 bsync({waitFor:[O(l[p[2]].x, l[p[2]].y)]});
6 bsync({request:[OWin]}, 100);
7 }
8 });
Listing 17. A b-thread that implements the O winning condition. Given a
permutation p and a line l (row, column, or diagonal), the b-thread waits for
three O events on the line, in the order specified by the permutation, and then
requests to announce that O wins the game.
1 bp.registerBThread("Clck("+r+","+c+")", function() {
2 while (true) {
3 bsync({waitFor:[Click(r,c)]});
4 bsync({request:[X(r,c)]});
5 }
6 });
Listing 18. A b-thread that implements the detection of user’s (player X)
click.
1 bp.registerBThread("GameEnd",function() {
2 bsync({waitFor: [OWin, XWin, draw]});
3 bsync({block: [X(0,0), X(0,1),...,O(2,2)]});
4 });
Listing 19. A b-thread that implements the requirement that no moves are
allowed once the game ends.

We now present the main part of the specification: a strategy for player O implemented by b-threads. While there are many implementations of strategies for this game, our approach here is to break the strategy to elements that correspond to the way parents teach their children how to win (or, at least,
avoid losing) the game. Arguably, we claim that people do not usually use the minimax algorithm that most computers are programmed to apply. Instead, we argue that most people use some set of intuitive rules of thumb. An example of a set of such rules is modeled by the b-threads below.

1 bp.registerBThread("Center",function() {
2 while (true)
3 bsync({request:[O(1,1)]},35);
4 });
Listing 20. A b-thread that implements the thumb-rule that, if no other thumbrule
applies, it is best to put an O in the center square.
1 bp.registerBThread("Corners",function() {
2 while (true)
3 bsync({request:[O(0,0),O(0,2),O(2,0),O(2,2)]},20);
4 });
Listing 21. A b-thread that implements the thumb-rule that, if no other thumbrule
applies, and the center square is taken, it is best to put an O in a corner
square.
1 bp.registerBThread("Sides",function() {
2 while (true) {
3 bsync({request:[O(0,1),O(1,0),O(1,2),O(2,1)]},10);
4 }
5 });
Listing 22. A b-thread that implements the thumb-rule that, if no other thumbrule
applies, and the center and all corner squares are taken, put an O in a
side square.







Note that the requests of the last three b-threads are with priorities 35, 20, and 10, respectively. These are the lowest priorities among all the b-threads that implement the thumbrules. This means that the event selection mechanism will only obey these requests if no other thumb-rule applies. It also means that we prefer to use the center over corners and corners over sides.
We proceed to describe the thumb-rules that relate to scenarios in the game:

1 bp.registerBThread("AddThirdO", function() {
2 while (true) {
3 bsync({waitFor:[ O(l[p[0]].x, l[p[0]].y)]});
4 bsync({waitFor:[ O(l[p[1]].x, l[p[1]].y)]});
5 bsync({request:[ O(l[p[2]].x, l[p[2]].y)]}, 50);
6 }
7 });
Listing 23. A b-thread that implements the thumb-rule of putting an O in a
line with two other O’s, in order to win the game. Given a permutation p and
a line l (row, column, or diagonal), the b-thread waits for two O events on
the line, in the order specified by the permutation, and then requests to mark
its final O.

Note that the priority of the AddThirdO b-thread is higher than the priority of PreventThirdX. This is because we prefer to win a game if possible.

1 bp.registerBThread("PreventThirdX", function() {
2 while (true) {
3 bsync({waitFor:[ X(l[p[0]].x, l[p[0]].y)]});
4 bsync({waitFor:[ X(l[p[1]].x, l[p[1]].y)]});
5 bsync({request:[ O(l[p[2]].x, l[p[2]].y)]}, 40);
6 }
7 });
Listing 24. A b-thread that implements the thumb-rule of putting an O in a
line with two X’s, in order to prevent a win of player X in the next move.
Given a permutation p and a line l (row, column, or diagonal), the b-thread
waits for two X events on the line, in the order specified by the permutation,
and then requests to mark an O on the third square.

The last type of thumb-rules in our strategy handle the so called “fork situations”, when player X tries to complete two lines at the same time. We only list one of them here, the PreventFork00X b-thread, that identifies one of the three ‘fork situations’. There are three more similar b-threads to handle
the other similar situations.

1 bp.registerBThread("PreventFork00X", function() {
2 while (true) {
3 bsync({waitFor:[X(f[p[0]].x, f[p[0]].y)]});
4 bsync({waitFor:[X(f[p[1]].x, f[p[1]].y)]});
5 bsync({request:[O(0,0),O(0,2),O(2,0)]}, 30);
6 }
7 });
Listing 25. A b-thread that implements the thumb-rule of preventing from
player X to complete two lines at the same time. Given a permutation p and
a “fork situation line” f (row or column), the b-thread waits for two X events
on the line, in the order specified by the permutation, and then requests to
mark an O on one of a given set of squares.

1 bp.registerBThread("PreventDiagForkX", function() {
2 while (true) {
3 bsync({waitFor:[X(f[p[0]].x, f[p[0]].y)]});
4 bsync({waitFor:[X(f[p[1]].x, f[p[1]].y)]});
5 bsync({request:[O(0,1),O(1,0),O(1,2),O(2,1)]},28);
6 }
7 });
Listing 26. A b-thread that implements the thumb-rule of preventing player
X from completing two lines at the same time using one of the diagonals.
Given a permutation p and a “fork situation diagonal’ f, the b-thread waits
for two X events on the diagonal, in the order specified by the permutation,
and then requests to mark an O on one of a given set of squares.


Notice that the b-threads in listings 15-17 and 20-26 involve the priority option so the application can best detect the situation its facing. For example, in listing 15-17, the DetectXWin and DetectOWin b-threads have priority 100 to ensure that the application detects these before it detects a draw. Also,
in listing 23, the priority of AddThirdO is higher than that of PreventThirdX because we want the application to prefer to win the game over a draw, or worse, giving the user (player X) another possibility to win the game in the next round (in case of a fork situation). The priority number is passed as an additional data to the bsync request. The additional data field is a general mechanism that can be used to attach meta-tdata, such as priorities, to synchronization statements. This data can,
as done here, be used by the event selection mechanism to guide its selections.
The Tic-Tac-Toe example shows that it is possible to maintain an intuitive one-to-one relation between requirements and b-threads. It also demonstrates the usage of a customized
event selection strategy, that takes priorities into account when selecting events.










Fig. 4. BPjs program stack, used for b-program execution. Parts that can
be provided by client code appear in white. The behavioral code (written
in JavaScript) is at the top level. This code can interact with its BPjs
infrastructure using a special object exposed by BPjs, called bp. BPjs runs
the standard JavaScript parts of the b-program code using the Mozilla Rhino
JavaScript engine. Event selection is done using an event selection strategy
object. When custom event selection logic is required, the host Java application
can provide a custom EventSelectionStrategy instance to BPjs. The
host application can interact with BPjs and the program it currently executes
using an API, and by pushing events to a queue. It can listen to event selections
and other b-program life cycle events by providing a listener object to the
BProgramRunner running the b-program.

Note that the priority event selection mechanism in BPjs is pluggable. Thus, programmers can implement and use other types of prioritization schemes instead of the default event selection strategy, which uses a random arbiter.

114 changes: 114 additions & 0 deletions docs/source/example-dining-philosophers.rst
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,114 @@
Example - Dining Philosophers

The Dining Philosophers is a classic concurrent programming challenge, first proposed as an exercise in an exam by Edsger Dijkstra in 1965. Imagine a group of philosophers, sitting at a round table. Each has a plate with food. For utensils, they have chopsticks - a single chopstick between each two plates (this setting correctly models the event budget of many Philosophy departments). In order to eat, each philosopher has to obtain both chopsticks adjacent to her.
The concurrency challenge is, of course, mutual exclusivity: A chopstick may only be held by a single philosopher at any given moment, and so they have to either coordinate, or experience hunger-induced existential crisis. This problem is illustrated in Figure 2.
The philosophers in our dining philosophers b-program use a naive algorithm, listed in Listing 4: a philosopher picks up the chopstick to their right, then the one to their left, eats, puts the left chopstick down, puts the right chopstick down, and then starts over again. While intuitive, this algorithm reaches a deadlock in a certain scenario we will automatically discover later.
The code in Listing 4 consists of a regular JavaScript function. This function adds the new b-thread to the b-program, based on the parameters it was invoked with. Functions like these can be viewed as parametrized b-thread templates. In this example, b-thread templates are used to reduce code
duplication. We now turn our attention to the chopsticks. In the modeled setting, each chopstick is shared by the two philosophers adjacent to it. Each of these philosophers can pick up and release said chopstick.
















Fig. 2. Dijkstra’s Dining Philosophers problem. Each two philosophers share
the chopstick between them. In order to eat, a philosopher has to pick up both
sticks. After eating, a philosopher releases the sticks and thinks. Since only
a single philosopher can use a stick at any given moment, this setting poses
many mutual exclusion challenges.
1 function addPhil(philNum) {
2 bp.registerBThread("Phil"+philNum, function() {
3 while (true) {
4 // Request to pick the right stick
5 bsync({
6 request: bp.Event("Pick"+philNum+"R")
7 });
8
9 // Request to pick the left stick
10 bsync({
11 request: bp.Event("Pick"+philNum+"L")
12 });
13
14 // Request to release the left stick
15 bsync({
16 request: bp.Event("Rel"+philNum+"L")
17 });
18
19 // Request to release the right stick
20 bsync({
21 request: bp.Event("Rel"+philNum+"R")
22 });
23 }
24 });
25 };
Listing 4. A function for adding a philosopher to the dining philosophers
b-program. A dining philosopher repeatedly attempts to pick the chopstick to
her right, then the one to her left, and then releases them in the same order.
For the purpose of this program, there’s no need to add an EAT or THINK
event.

Some restriction apply, though: a philosopher can only pick up a chopstick when it lays on the table, and can only release a chopstick after picking it up. Additionally, a chopstick can be picked up by at most a single philosopher at a time. Consequentially, if one philosopher have picked a chopstick up, the other philosopher has to wait for the first philosopher to release the chopstick, prior to picking it up herself. Imposing these constraints is done by the chopstick b-thread. The code for adding a these b-threads is shown in Listing 5. The implementation of chopstick b-threads demonstrates some interesting features of BP and BPjs. First, note the usage of event sets in lines 5 and 9. These are used to detect the pick up and release event of the stick being modeled.

1 function addStick(i) {
2 var j = (i%PHILOSOPHER_COUNT)+1;
3
4 bp.registerBThread("Stick"+i, function () {
5 var pickMe = bp.EventSet("pick"+i, function(e) {
6 return (e.name === "Pick"+i+"R"
7 jj e.name === "Pick"+j+"L");
8 });
9 var releaseMe = [bp.Event("Rel"+i+"R"),
10 bp.Event("Rel"+j+"L")];
11
12 while (true) {
13 var e = bsync({waitFor: pickMe,
14 block: releaseMe});
15
16 var wt = (e.name === "Pick"+i+"R") ?
17 "Rel"+i+"R" : "Rel"+j+"L";
18 bsync({waitFor: bp.Event(wt),
19 block: releaseMe});
20 }
21 });
22 }
Listing 5. A function for adding a chopstick to the dining philosophers bprogram. This b-thread ensures that the chopstick it models can be picked up by at most a single philosopher at a time. Note the usage of event sets for detecting Pick and Release events — this is needed, since philosophers adjacent to a stick refer to it using different names. For example, the stick between philosophers 3 and 4 would be referred to as 3R by philosopher 3, and 4L by philosopher 4.

The philosophers adjacent to a stick refer to it using different names. Thus, picking up stick #2 can be done using events Pick2R or Pick3L. These events are contained in the pickMe event set defined in line 5. Set membership is determined by examining the event name, which is a regular JavaScript string
object. Event sets created in BPjs are similar to mathematical sets: a predicate over events (although BPjs allows naming them too). Unlike set implementations in common collection frameworks, it is impossible to iterate over their members. Consequentially, it is meaningless to request such an event set during a bsync. doing so will cause BPjs’ runtime engine to throw an error.
The releaseMe event set, on the other hand, is an array of event objects. When such arrays are passed to bsync , they are treated as an event set. This type of event set can be requested during a bsync, using the same syntax for requesting a single event. The exact semantics of requesting an event array are decided by the event selection strategy. It can ignore the order of elements, giving the array mathematical set semantics. Alternatively, it can consider the order of elements and select the first element that is not blocked by other bthreads, giving the array preference queue semantics. Event
selection strategies are covered in detail in Subsection VIII-A.
Having described the philosophers and chopsticks, it is now time to bring them all to the table. This is done using a regular JavaScript loop, shown in Listing 6.

Discussion: The dining philosophers b-program described here can serve both as a simulation program and as a model to be checked. For simulation purposes, this b-program is run (see Section V), and its event log can be analyzed, e.g. to get statistics about stick wait times. For verification, the b-program
is passed to a verification engine, as shown in Section VI.

1 if (!PHILOSOPHER_COUNT) PHILOSOPHER_COUNT = 5;
2
3 for (var i=1; i<=PHILOSOPHER_COUNT; i++) {
4 addStick(i);
5 addPhil(i);
6 }
Listing 6. The loop instantiating a dining philosophers model. If
PHILOSOPHER_COUNT was not passed by the containing Java application,
it defaults to 5.
Fig. 3. A maze, described using our maze-description DSL (left), and a maze
solution, found by a generic b-program model checker (right). The model
checker output, an event sequence, was post-processed by the program to
visualize the solution on the maze’s map.
In both cases, the exact same code is used — no translation
is necessary when transitioning between code execution and
verification.


This example uses parametrized templates to create its bthreads. B-thread templates are a versatile and commonly used design pattern, applicable in various contexts. When creating simulations, b-thread templates can be used to generate heterogeneous b-thread population, where the template parameters are sampled from a given distribution. In the next section, they are used to create an interpreter for a small DSL.

Loading

0 comments on commit 10a2a33

Please sign in to comment.