User's Manual

In SyncGen, the developer builds core functional code without implementing the synchronization policy. For example, in a readers/writers system, code to access a shared buffer would be written as shown below:


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 ) {
            System . out . println ( "reader reading:" ) ;
            System . out . println ( "done reading" ) ;
        }
    }
}

final class Writer extends Thread {
    public void run ( ) {
        while ( true ) {
            System . out . println ( "writer writing:" ) ;
            System . out . println ( "done writing" ) ;
        }
    }
}



The developer delimits particular code regions that will be synchronized. In the example above, one would mark the region that reads shared data and named this region "Reader" and the region that modify or write the data and named this region "Writer". The core functional code with marks is listed as below:


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 ***/
        }
    }
}


The "RW" in the marks is a cluster name. Clusters are partitions of regions. Intuitively, a cluster consists of all the related regions. For example, the Reader region and Writer region share data, thus they are in the same cluster and we named it "RW" in the above example.

Now the task before the developer is to specify a synchronization policy that controls the scheduling of threads that attempt to execute in those regions. In SyncGen, synchronization policies are stated as global invariants. The easiest way to specify a global invariant in SyncGen is to use SyncGen's Synchronization Pattern system. Two of the simplest patterns are Exclusion and Bound:

  • Bound(R,n): at most n threads can be in region R at any point in time.
  • Exclusion (R_1, R_2, ..., R_n): at any point in time, threads can be in at most one synchronization region out of the n synchronization regions.

We can use these patterns to state a synchronization policy for the Readers/Writers problem as follows.


Exclusion(Reader,Writer) + Bound(Writer,1)

The intuition here is that reader and writer threads can not be both present in their regions at the same time and at most one writer thread can be in Writer region.

In the SyncGen tool, the pattern for the synchronization policy must be put in a file, for example, the file for the readers/writers problem is listed as follows.


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


From this specification, SyncGen can generate an implementation (e.g., in Java) to realize the synchronization policy.

As an intermediate step, SyncGen generates what is called a coarse grain solution. The coarse-grain solution states the semantics of the synchronization solution in a language of guarded commands. This provides a source-language independent definition of the synchronization semantics. For example, here is the coarse-grain solution for the readers/writers example:


CLUSTER: RW
STATE SPACE VARIABLES: Writer_in,Reader_out,Reader_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;


The solution passes along the declared cluster and region names, gives the await/atomic statement associated with each region entrance/exit, and specifies other regions that should be notified upon completion of each region entrance/exit. The intuition behind the guards for each region entrance is as follows: the reader region can only be entered when there are no threads present in the writer region (i.e., when the difference between the number of threads that have entered the writers region and the number of threads that have exited the writers region is zero), and the writer region can only be entered when (a) there are no threads present in the reader region and (b) there are no threads present in the writer region.

An implementation (Java/C/C++) can be automatically synthesized by SyncGen from the coarse grain solution. For example, the Java implementation of  the readers/writers example is listed  as below:


class SGCluster$RW {
// STATE SPACE VARIABLES:
private static int Writer_in,Reader_out,Reader_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.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();
   }
}
}


The Java implementation generates a class for each cluster named it as SGCluster$clname, where clname is the cluster name.  All the state variables in the coarse grain solution are turned into static fields and
each await/atomic statement is turn into one or two static methods of the class.

Finally, the calls to the automatically generated implementation are weaved in the core functional code at each special mark that user indicates for each entry and exit of all regions. For example, here is the readers/writers problem's core functional code after weaving:


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 ) {
            SGCluster$RW.Reader$enter();
            System . out . println ( "reader reading:" ) ;
            System . out . println ( "done reading" ) ;
            SGCluster$RW.Reader$exit();
        }
    }
}

final class Writer extends Thread {
    public void run ( ) {
        while ( true ) {
            SGCluster$RW.Writer$enter();
            System . out . println ( "writer writing:" ) ;
            System . out . println ( "done writing" ) ;
            SGCluster$RW.Writer$exit();
        }
    }
}


The develop now has a complete system!