A COO System:
The Table of Dynamic Philosophers

 

 

The Dynamic Philosophers have been used as a case study at the 2nd Workshop on Object-Oriented Programming and Models of Concurrency

Statement of the case

The case is a refinement of the well known dinning philosophers example. Some philosophers are around a table. Each one has his plate, and he shares a fork with his right neighbour and a fork with his left neighbour.

  1. When a philosopher doesn't has his left fork, he can call his left neighbour for this fork, and the same holds for his right fork;
  2. When a philosopher has his right fork and has received a request for this fork, he must give it to his right neighbour, and the same holds for his left fork;
  3. a philosopher can eat only when he has two forks;
  4. some philosophers have the additional capability to introduce a new guest; when a new philosopher arrives at the table, he has one plate and one fork coming from a heap of forks;
  5. some philosophers (possibly the same ones) have the additional capability to leave the table; when a philosopher leaves the table, he goes with his plate and one fork, and put the fork into the fork’s heap.
  6. . each philosopher behaves in such a way that the whole system is fair: philosophers eat in turn;
  7. in any case, there is at least two philosophers at the table.
The Static Philosopher and Heap classes will be first introduced, and then the Dynamic one.

The Static Philosopher class

The behaviour of a Static Philosopher, shown in Figure 1, is quite simple.

When he has his left and right forks (places LFork and RFork), a philosopher may starteating and then stopeating. When he has its right fork, his GiveRFork service is available, and when he has no right fork he can request his left neighbour for the GiveLFork service, and the same holds at his left side. Thus he only needs to know the name of his two neighbours. Graphically, accept- and result-places of services do not appear in the OBCS, but transitions which accept a service or return its result are pointed out by a dangling arc labelled with the appropriate parameters. In the Philosopher case, each service is accepted and returned by the same transition.

The LNMayLeave, NewLN and NewRN services are not implemented into the SPhilo class. But they are there in order to enable the Dynamic Philosopher class to inherit the SPhilo class without having to redefine the type of the rn and ln attributes.

class SPhilo specification;
uses fork, Bool;
attributes
rn : SPhilo*; //the right and left neighbours
ln : SPhilo*;
operations
Init (n: const OCNAME, l: SPhilo*, r: SPhilo*, f: fork) ///
setname (n);
ln = l; rn = r; nbeating = 0;
NoLFork.ADDTOKEN (NoLFork.MakeToken ());
RFork.ADDTOKEN (RFork.MakeToken (f));
///;
services
GiveLFork (): <fork>;
GiveRFork (): <fork>;
LNMayLeave (): <Bool>; //the Lef Neighbour Maay Leave
NewLN (phil: Philo*); //there is a New Left Neighbour
NewRN (phil: Philo*);
OBCS //for documentation purpose only
end.
 
class SPhilo implementation;
attributes
nbeating : short; //counts how many times the Phil. eats
OBCS //as edited using MACAO
end.
Figure 1: definition of the Static Philosopher class
 
class Heap specification;
uses fork, Bool;
operations
Init (nbfork: int, n: const OCNAME) ///
setname (n);
philnum = 0;
for (fork i = 1; i <= nbfork; i++)
FreeForks.ADDTOKEN (FreeForks.MakeToken (i));
///;
services
Take (f : fork);
Give () : <int, fork>;
end.
 
class Heap implementation;
attributes
philnum: int; //to give a new number to each Philosopher
OBCS
end.
Figure 2: definition of the Heap class

 

A table of Dynamic Philosophers

To ensure the boundedness of a table of Dynamic Philosophers, the number of forks is limited, and they are kept by an object of class Heap. Thus, a Philosopher may be introduced at the table only if the heap supplies a fork, and a leaving Philosopher has to give his fork back. Its results from the OBCS of this class that the Give service is always available (See Figure 2). If it would not be the case, it could happen that all the philosophers around the table are blocked while waiting for a fork.

As far as eating and the exchange of forks is concerned, a Dynamic Philosopher behaves as a static one, so that the DPhilo class may inherit the SPhilo one. But with regard to joining and leaving the table, the logic of the Dynamic Philosophers is more complex and the DPhilo class must be designed in such a way that the two following requirements are ensured at any moment:

R1: one and only one fork is shared by tow adjoining Philosophers;

R2: every request sent to a neighbour is actually received and replied by the sender’s neighbour, that is it must never happen that:

  • a request is sent to a leaving Philosopher which will never reply, or
  • a new Philosopher is introduced between the sender and his previous neighbour.
    •  R1 is quite easy to ensure, for instance by means of the following policy:

    (1): a Philosopher joins or leaves the table

    The R2 requirement is much more difficult to ensure in the absence of a centralised control. Namely, it means that there is no concurrent moves at two adjacent places around the table. For instance, let consider two adjoining Philosophers fl and fr, and fl’ and fr’ be concurrently introduced between them; fl’ and fr’ will both have a reference toward fl as their left neighbour and toward fr as their right neighbour, and this is clearly wrong. Thus, if fl is at the left side of fr, the following cases must be avoided: Among the policies which ensure that these cases never occur, we choose the following one:

    (2): a Philosopher may join the table only if he is introduced by an already installed colleague, and he seats at his left side (so c1 is avoided);

    (3): a Philosopher may not concurrently introduce a colleague and leaves (c4 avoided);

    (4): when he intends to leave, a philosopher must ask his right neighbour for the permission to leave; this latter refuses if he himself is leaving or introducing, and when he accepts, he is prevented from leaving and introducing until he knows his new left neighbour (c2 and c3 avoided).

     

    class DPhilo specification;
    inherits SPhilo;
    refers Heap;
    attributes
    h : Heap*;
    operations
    Init (id: int, l: DPhilo*, r: DPhilo*, f: fork, hp: Heap*) ///
    setname ("Philo",id);
    ln = l; rn = r; h = hp;
    delayquit = rand() % 4; delayint = rand()% 6;
    nbeating = 0;
    NoLFork.ADDTOKEN (NoLFork.MakeToken ());
    RFork.ADDTOKEN (RFork.MakeToken (f));
    ///;
    end.
     
    class DPhilo implementation;
    attributes
    delayquit: short; //to make DPhilos a bit steady
    delayint: short;
    operations
    //may be interactivelly called from the debugger
    Display (pr: TrInstance, next: TrInstance) ///
    printf ("PHILOSOPHER %s has eaten %d\n",_name, nbeating);
    printf ("left neighb: %s, right neighb: %s\n",
    ln->_name, rn->_name);
    ///;
    OBCS //places and transitions of the SPhilo class are not shown

    Figure 3: Definition of the DPhilo class

    It results from (1) and (2) that a Philosopher can introduce only when his NoLeftFork place has a token, and from (1) that he can try to leave only when his NoLeftFork and RightFork places have a token. Thus, the mutual exclusion of leaving and introducing (3) is enforced by the NoLeftFork place. Referring to the permission to leave as the LeftNeighbMayLeave service, it must be permanently available to prevent the system from blocking in case all Philosophers simultaneously intend to leave. The result of the above remarks and (4) is that this service has to supply a Yes answer when the NoLeftFork place contains a token, and a No answer when it is empty.

    The OBCS of the DPhilo class shown in Figure 3 implements this policy.

     

    The Stack example

    Overview of COOs, SYROCO

    Mail to: C. Sibertin-Blanc