views:

60

answers:

2

Is there any other documentation/discussion about the following design pattern (I'm not sure what it is called) from a well-known source? I'm almost 100% sure that the following will manage data safely between two (not more than two) processes, but would feel much better if I could find some more detailed information on why it works from a reputable source.


Suppose I have two processes A and B that are executing in parallel. They share the following data structure (in pseudo-C code):

struct Shared
{
    bool ownedByA
    Otherstuff otherstuff;
}

I can use the following pair of state machines to manage this shared data safely:

A:

state A.A (data is owned by A), entered on startup:
    read/modify/write "otherstuff"
    when done, goto A.Adone

state A.Adone
    set ownedByA to false
    goto state A.B

state A.B (data is owned by B):
    if ownedByA is true, goto state A.A
    otherwise stay in state A.B

B:

state B.A (data is owned by A), entered on startup:
    if ownedByA is false, goto state B.B
    otherwise stay in state B.A

state B.B (data is owned by B):
    read/modify/write "otherstuff"
    when done, go to B.Bdone

state B.Bdone:
    set ownedByA to true
    goto state B.A

We must ensure A.A's writes to "otherstuff" and A.Adone's write to ownedByA are in strict sequence ordering w/r/t memory visibility. Similarly for B.B and B.Bdone.

at startup:

1. Initialize ownedByA to true, A to the A.A state, B to the B.A state
2. start running state machines 
(ensure that 1. happens-before 2.)
+1  A: 

Maybe that's a Dining philosophers problem with only two philosophers and one fork.

http://en.wikipedia.org/wiki/Dining_philosophers_problem

nanda
+1  A: 

You can try Th. J. Dekker's solution, mentioned by E. W. Dijkstra in his EWD1303 paper. alt text

And then something profound and lovely happened. By analyzing by what structure of argument the proof obligations could be met, the numerical mathematician Th.J. Dekker designed within a few hours
the above solution together with its correctness argument, and this settled the contest.
In the above solution, the pair "c1,c2" implements the mutual exclusion, while "turn" has been introduced to resolve the tie when the two processes simultaneously try to enter their critical sections.

Nick D
yay! cool, most good concurrency algorithms trace back to or through Edsgar Dijkstra.
Jason S
Consider adding a link to the wikipedia page for Dekker's algorithm: http://en.wikipedia.org/wiki/Dekker%27s_algorithm
Jason S
@Jason, done. I forgot to look on Wikipedia.
Nick D
Interesting -- I've been staring at information on Dekker's algorithm to try to figure out the differences between this and what I wrote above (why does he need 3 flags and I only have 1), and it looks like in my case there are 2 overall "ownership" states (depending on the "ownedByA" flag) with some additional transients, whereas in Dekker's algorithm there are 3 "ownership" states (either nobody is in a critical section, or process 1 is, or process 2 is). Maybe I'll call mine the "hot potato" algorithm. :-)
Jason S
Ah: a further read into Dijkstra's "Cooperating Sequential Processes" shows the first solution in section 2.1 (http://www.cs.utexas.edu/users/EWD/transcriptions/EWD01xx/EWD123.html#2.1.%20A%20Simple%20Example%2e) is what I was looking for. This is deemed unacceptible to Dijkstra because it ping-pongs between processes 1 and 2 synchronously, but for my purposes it does what I want within my state machines. Answer accepted because it is really close + got me to the right place, along w/ learning other information.
Jason S
@Jason, IMO it's better to post the above comment as an answer to your question, and accept it later. Anyway, EWD papers are cool and full of gems :)
Nick D