Fischer Protokoll

- wechselseitiger Ausschluss für den Zugriff auf eine
  kritische Region, mit N Prozessen
- Kommunikation über shared memory, atomares read und write,
  write benötigt a Zeiteinheiten
- gemeinsame Variable k


- Prozess 1 pid=1, Prozess pid=2, usw. 
- jetzt: zwei Prozesse

-------------------------------------------------------------

void process(int i)
{
  while(1)
  {
    do
    {
      waitfor( k == 0); //warten, bis k==0 ist
      
      k = i;            //k auf pid setzen, kostet a Zeit-
                        //einheiten
      wait(b);          //b > a 
    } while(k != i)     //warten, solange k nicht meine pid 
                        //ist
    //critical section

    k = 0;              //Zugriff wieder erlauben
  }
} 

-------------------------------------------------------------

-- Spezifikation mit Timed CSP

channel lese_k, schreibe_k : {0,1,2}
channel critical_section : {1,2}

VAR(value) = lese_k!value -> VAR(value)
            []
             schreibe_k?newValue -> Wait a; VAR(newValue)

VARPROCESS = VAR(0)


PROCESS(i) = WARTEN2(i);
             critical_section!i ->
	     schreibe_k!0 ->
	     PROCESS(i)

WARTEN = lese_k?k ->
         if (k == 0) then SKIP
	 else Wait 1; WARTEN

WARTEN2(i) = WARTEN;
             schreibe_k!i ->
	     Wait b;
             lese_k?k ->
             if(k == i) then SKIP
	     else WARTEN2(i)

SYSTEM = VARPROCESS
        [| {| schreibe_k, lese_k |} |]
         (||| i:{1,2} @ PROCESS(i)) 

-- PROCESS(1) ||| PROCESS(2)