Reader Writer Problem


Description

The problem consists of readers and writers that share a data resource. The readers only want to read from the resource, the writers want to write to it. Obviously, there is no problem if two or more readers access the resource simultaneously. However, if a writer and a reader or two writers access the resource simultaneously, the result becomes indeterminable. Therefore the writers must have exclusive access to the resource.

Diagram

Basically, reader and writer entrance are synchronization regions. Reader and writer are mutual excluded. And writer region has bound one.
.

Synchronization Specification


Cluster: RW ;
Regions: Reader, Writer;
Invariant: Exclusion(Reader,Writer) + Bound(Writer,1) ;

Patterns Used

Exclusion and Bound

Global Invariant

Unbounded Global Invariant

(R_in - R_out == 0 or W_in - W_out == 0) and (W_in - W_out <= 1)

Bounded Global Invariant Counter Version

(E1_0 == 0 or E1_1 == 0) and (B1 <= 1)

Core Functional Code

class RW$fine
{
    public static void main ( String argv [ ] )

    {
        new Reader ( ) . start ( ) ;

        new Reader ( ) . start ( ) ;

        new Writer ( ) . start ( ) ;

        new Writer ( ) . start ( ) ;

    }
}

final class Reader extends Thread
{

    public void run ( )
    {
        while ( true )

        {

            /*** RW Reader enter ***/
            System . out . println ( "reader reading:" ) ;

            System . out . println ( "done reading" ) ;

            /*** RW Reader exit ***/
        }
    }
}

final class Writer extends Thread

{
    public void run ( )
    {
        while ( true )

        {
            /*** RW Writer enter ***/
            System . out . println ( "writer writing:" ) ;

            System . out . println ( "done writing" ) ;

            /*** RW Writer exit ***/
        }
    }
}

Unbounded Coarse-Grain Solution

CLUSTER: RW
STATE SPACE VARIABLES: Reader_in, Reader_out, Writer_in, Writer_out;
REGION: Reader
ENTER: <AWAIT Writer_in == Writer_out --> Reader_in++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <Reader_out++;>
NOTIFY: ;
NOTIFYALL: Writer_in;

REGION: Writer
ENTER: <AWAIT Reader_in == Reader_out && Writer_in == Writer_out --> Writer_in++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <Writer_out++;>
NOTIFY: Writer_in;
NOTIFYALL: Reader_in;

Bounded Counter Coarse-Grain Solution

CLUSTER: RW
STATE SPACE VARIABLES: E1_0, E1_1, B1;
LOCAL VARIABLES: ;
REGION: Reader
ENTER: <AWAIT E1_1 == 0 --> E1_0++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <E1_0--;>
NOTIFY: ;
NOTIFYALL: Writer_in;

REGION: Writer
ENTER: <AWAIT E1_0 == 0 && B1 == 0 --> E1_1++;B1++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <E1_1--;B1--;>
NOTIFY: Writer_in;
NOTIFYALL: Reader_in;

Unbounded Fine-Grain Solution


class SGCluster$RW {

    // counter for Reader region:
    private static int Reader_in, Reader_out;

    // counter for Writer region:

    private static int Writer_in, Writer_out;

    private static Object clusterCounterLock = new Object();


    /**======================================================**
     **
     ** Generated lock and methods for await: Reader$enter
     **
     **======================================================**/

    private static Object condition$Reader$enter = new Object();

    public static void Reader$enter(){
        synchronized (condition$Reader$enter) {

            while ( !check$Reader$enter())
                try {

                    condition$Reader$enter.wait();
                } catch (InterruptedException e){}

        }

    }
    private static boolean check$Reader$enter() {

        synchronized (clusterCounterLock) {
            if (Writer_in == Writer_out ) {

                Reader_in ++ ;
                return true;
            } else

                return false;
        }
    }
    /**======================================================**
     **
     ** Generated lock and methods for atomic: Reader$exit
     **
     **======================================================**/

    public static void Reader$exit() {

        synchronized (clusterCounterLock) {
            Reader_out ++ ;

        }
        synchronized (condition$Writer$enter) {
            condition$Writer$enter.notify();

        }


    }


    /**======================================================**
     **
     ** Generated lock and methods for await: Writer$enter
     **
     **======================================================**/

    private static Object condition$Writer$enter = new Object();

    public static void Writer$enter(){
        synchronized (condition$Writer$enter) {

            while ( !check$Writer$enter())
                try {

                    condition$Writer$enter.wait();
                } catch (InterruptedException e){}

        }

    }
    private static boolean check$Writer$enter() {

        synchronized (clusterCounterLock) {
            if (Reader_in == Reader_out && Writer_in == Writer_out ) {

                Writer_in ++ ;
                return true;
            } else

                return false;
        }
    }
    /**======================================================**
     **
     ** Generated lock and methods for atomic: Writer$exit
     **
     **======================================================**/

    public static void Writer$exit() {

        synchronized (clusterCounterLock) {
            Writer_out ++ ;

        }
        synchronized (condition$Writer$enter) {
            condition$Writer$enter.notify();

        }

        synchronized (condition$Reader$enter) {

            condition$Reader$enter.notifyAll();
        }


    }

}

 

Bounded Fine-Grain Solution


class SGCluster$RW {

// STATE SPACE VARIABLES: 
private static int Reader_in , Reader_out , Writer_in , Writer_out ;

// LOCAL VARIABLES: 

private static Object clusterCounterLock = new Object();


/**======================================================**
 **
 ** Generated lock and methods for await: Reader$enter
 **
 **======================================================**/

private static Object condition$Reader$enter = new Object();

public static void Reader$enter(){
   synchronized (condition$Reader$enter) {

      while ( !check$Reader$enter())
         try {

            condition$Reader$enter.wait();
         } catch (InterruptedException e){}

   }

}
private static boolean check$Reader$enter() {

   synchronized (clusterCounterLock) {
      if (Writer_in == Writer_out ) {

         Reader_in ++ ; ;
         return true;
      } else

         return false;
   }
}
/**======================================================**
 **
 ** Generated lock and methods for atomic: Reader$exit
 **
 **======================================================**/

public static void Reader$exit() {

   synchronized (clusterCounterLock) {
      Reader_out ++ ; ;

   }
   synchronized (condition$Writer$enter) {
      condition$Writer$enter.notifyAll(); 
   }


}


/**======================================================**
 **
 ** Generated lock and methods for await: Writer$enter
 **
 **======================================================**/

private static Object condition$Writer$enter = new Object();

public static void Writer$enter(){
   synchronized (condition$Writer$enter) {

      while ( !check$Writer$enter())
         try {

            condition$Writer$enter.wait();
         } catch (InterruptedException e){}

   }

}
private static boolean check$Writer$enter() {

   synchronized (clusterCounterLock) {
      if (Reader_in == Reader_out && Writer_in == Writer_out ) {

         Writer_in ++ ; ;
         return true;
      } else

         return false;
   }
}
/**======================================================**
 **
 ** Generated lock and methods for atomic: Writer$exit
 **
 **======================================================**/

public static void Writer$exit() {

   synchronized (clusterCounterLock) {
      Writer_out ++ ; ;

   }
   synchronized (condition$Writer$enter) {
      condition$Writer$enter.notify(); 
   }

   synchronized (condition$Reader$enter) {
      condition$Reader$enter.notifyAll(); 
   }


}

}