Peterson's algorithm freezes the browser -- but it works!
Chris Pressey
10 years ago
| 98 | 98 |
(This doesn't entirely make sense if `WAIT` is the final instruction in
|
| 99 | 99 |
a program, though.)
|
| 100 | 100 |
|
|
101 |
Advanced Examples
|
|
102 |
-----------------
|
|
103 |
|
|
104 |
There are some classic synchronization algorithms in computer science.
|
|
105 |
We can try some of them here, and see if Matchbox can tell us if they
|
|
106 |
work.
|
|
107 |
|
|
108 |
[Peterson's algorithm][] is implemented in `eg/petersons-no-race.mbox`.
|
|
109 |
Inside the critical sections, the programs shown above, the ones which
|
|
110 |
have the race condition, are embedded. Matchbox takes a while to find
|
|
111 |
all the interleavings, but once it does, it confirms that there is no
|
|
112 |
race condition.
|
|
113 |
|
|
114 |
[Dekker's algorithm][] will not be possible to implement in Matchbox,
|
|
115 |
because it contains a nested `while` loop (see "Limitations", below.)
|
|
116 |
|
| 101 | 117 |
Discussion
|
| 102 | 118 |
----------
|
| 103 | 119 |
|
|
| 146 | 162 |
|
| 147 | 163 |
* animate and basically display it all more nicely
|
| 148 | 164 |
* ability to break on first inconsistent result (for long programs)
|
| 149 | |
* add sufficient instructions to implement:
|
| 150 | |
|
| 151 | |
* [Peterson's algorithm][]
|
| 152 | |
* maybe [Szymanski's algorithm][]
|
| 153 | |
|
| 154 | |
[Dekker's algorithm][] will not be possible, because it contains a
|
| 155 | |
nested `while` loop.
|
|
165 |
* add sufficient instructions to implement [Szymanski's algorithm][]?
|
| 156 | 166 |
|
| 157 | 167 |
[race conditions]: http://en.wikipedia.org/wiki/Race_condition
|
| 158 | 168 |
[Dekker's algorithm]: http://en.wikipedia.org/wiki/Dekker%27s_algorithm
|
|
0 |
PROG 0
|
|
1 |
; M0 is flag[0]
|
|
2 |
; M1 is flag[1]
|
|
3 |
; M2 is turn
|
|
4 |
; M3 is the target
|
|
5 |
|
|
6 |
MOV 1, M0
|
|
7 |
MOV 1, M2
|
|
8 |
WAIT M1, 0
|
|
9 |
WAIT M2, 0
|
|
10 |
|
|
11 |
; begin c.s.
|
|
12 |
MOV M3, R0
|
|
13 |
INC R0
|
|
14 |
MOV R0, M3
|
|
15 |
; end c.s.
|
|
16 |
|
|
17 |
MOV 0, M0
|
|
18 |
|
|
19 |
PROG 1
|
|
20 |
; M0 is flag[0]
|
|
21 |
; M1 is flag[1]
|
|
22 |
; M2 is turn
|
|
23 |
; M3 is the target
|
|
24 |
|
|
25 |
MOV 1, M1
|
|
26 |
MOV 0, M2
|
|
27 |
WAIT M0, 0
|
|
28 |
WAIT M2, 0
|
|
29 |
|
|
30 |
; begin c.s.
|
|
31 |
MOV M3, R0
|
|
32 |
INC R0
|
|
33 |
MOV R0, M3
|
|
34 |
; end c.s.
|
|
35 |
|
|
36 |
MOV 0, M1
|
| 37 | 37 |
output.innerHTML = matchbox.run(prog1ta.value);
|
| 38 | 38 |
});
|
| 39 | 39 |
yoob.makeLineBreak(prog1Ctr);
|
| 40 | |
var prog1ta = yoob.makeTextArea(prog1Ctr, 20, 10);
|
|
40 |
var prog1ta = yoob.makeTextArea(prog1Ctr, 20, 20);
|
| 41 | 41 |
|
| 42 | 42 |
var prog2Ctr = makeContainer();
|
| 43 | 43 |
var run2Btn = yoob.makeButton(prog2Ctr, "Run", function() {
|
| 44 | 44 |
output.innerHTML = matchbox.run(prog2ta.value);
|
| 45 | 45 |
});
|
| 46 | 46 |
yoob.makeLineBreak(prog2Ctr);
|
| 47 | |
var prog2ta = yoob.makeTextArea(prog2Ctr, 20, 10);
|
|
47 |
var prog2ta = yoob.makeTextArea(prog2Ctr, 20, 20);
|
| 48 | 48 |
|
| 49 | 49 |
var resultCtr = makeContainer();
|
| 50 | 50 |
var findRacesBtn = yoob.makeButton(
|
|
| 67 | 67 |
});
|
| 68 | 68 |
p.add('basic-race.mbox');
|
| 69 | 69 |
p.add('basic-no-race.mbox');
|
|
70 |
p.add('petersons-no-race.mbox');
|
| 70 | 71 |
p.select('basic-race.mbox');
|
| 71 | 72 |
|
| 72 | 73 |
};
|