User Tools

Site Tools


calendar

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
calendar [2009/04/26 19:38] franckcalendar [2009/05/14 21:04] (current) franck
Line 80: Line 80:
 If you come across another source that may be useful, please email it to the instructor. If you come across another source that may be useful, please email it to the instructor.
  
-<code java> +simple example of a concurrent Java program can be found 
-/** +[[printer|here]].
- printer prints its name 1000 times. +
- * +
- * @author Franck van Breugel +
- */ +
-public class Printer extends Thread +
-+
-  /** +
-   * Initializes this printer with the given name. +
-   * +
-   * @param name the name of this printer. +
-   * @pre. name != null +
-   */ +
-  public Printer(String name) +
-  { +
-    super(name); +
-  } +
- +
-  /** +
-   * Prints the name of this printer 1000 times. +
-   */ +
-  public void run() +
-  { +
-    final int NUMBER = 1000; +
-    for (int i = 0; i < NUMBER; i++) +
-    { +
-      System.out.print(this.getName()); +
-    } +
-  } +
-+
-</code> +
- +
-<code java> +
-public class PrinterTest +
-+
-  public static void main(String[] args) +
-  { +
-    new Printer("1").start(); +
-    new Printer("2").start(); +
-  } +
-+
-</code> +
- +
-<code java> +
-/** +
- * A printer prints its name 1000 times. +
- * +
- * @author Franck van Breugel +
- */ +
-public class Printer implements Runnable +
-+
-  public void run() +
-  { +
-    final int NUMBER = 1000; +
-    for (int i = 0; i < NUMBER; i++) +
-    { +
-      System.out.print(Thread.currentThread().getName()); +
-    } +
-  } +
-+
-</code> +
- +
-<code java> +
-public class PrinterTest +
-+
-  public static void main(String[args) +
-  { +
-    Printer printer = new Printer(); +
-    new Thread(printer, "1").start(); +
-    new Thread(printer, "2").start(); +
-  } +
-+
-</code>+
  
 ===== March 31 ===== ===== March 31 =====
  
-A solution to the readers-writers problem using semaphores in Java+Implementations in Java of the reader-writers problem can be 
-First, a Reader. +found [[readers-writers|here]].
-<code java> +
-package semaphore; +
-  +
-import java.util.Random; +
-import java.util.concurrent.Semaphore; +
-  +
-/** +
- * A reader+
- * +
- * @author Franck van Breugel +
- */ +
-public class Reader extends Thread +
-+
-  private static int readers = 0; +
-  private static final Semaphore mutex = new Semaphore(1); +
-      +
-  /** +
-   * Initializes this reader. +
-   */ +
-  public Reader() +
-  { +
-    super(); +
-  } +
-                                                                                 +
-  /** +
-   * Reads. +
-   */ +
-  public void run() +
-  { +
-    try +
-    { +
-      Reader.mutex.acquire(); +
-      Reader.readers++; +
-      if (Reader.readers == 1) +
-      { +
-        Writer.writer.acquire(); +
-      } +
-      Reader.mutex.release(); +
-      // read +
-      Reader.mutex.acquire(); +
-      Reader.readers--; +
-      if (Reader.readers == 0) +
-      { +
-        Writer.writer.release(); +
-      } +
-      Reader.mutex.release(); +
-    } +
-    catch (InterruptedException e) {} +
-  } +
-+
-</code> +
-Then, a Writer. +
-<code java> +
-package semaphore; +
-  +
-import java.util.Random; +
-import java.util.concurrent.Semaphore; +
-  +
-/** +
- * A writer. +
- * +
- * @author Franck van Breugel +
- */ +
-public class Writer extends Thread +
-+
-  public static final Semaphore writer = new Semaphore(1, true); +
-     +
-  /** +
-   * Initializes this writer. +
-   */ +
-  public Writer() +
-  { +
-    super(); +
-  } +
-      +
-  /** +
-   * Writes. +
-   */ +
-  public void run() +
-  { +
-    try +
-    { +
-      Writer.writer.acquire(); +
-      // write +
-      Writer.writer.release(); +
-    } +
-    catch (InterruptedException e) {} +
-  } +
-+
-</code> +
-And finally an app. +
-<code java> +
-package semaphore; +
-  +
-/** +
- * This app creates a number of readers and writers. +
- +
- * @author Franck van Breugel +
- */ +
-public class ReadersWriters +
-+
-  /** +
-   * @param args[0] numbers of readers+
-   * @param args[1] number of writers+
-   */ +
-  public static void main(String[args) +
-  { +
-    try +
-    { +
-      int readers = Integer.parseInt(args[0]); +
-      int writers = Integer.parseInt(args[1]); +
-      for (int i = 0; i < writers; i++) +
-      { +
-        new Writer().start(); +
-      } +
-      for (int i = 0; i < readers; i++) +
-      { +
-        new Reader().start(); +
-      } +
-    } +
-    catch (Exception e) +
-    { +
-      System.out.println("Usage: java ReadersWriters < number of readers> <number of writers>"); +
-    } +
-  } +
-+
-</code> +
- +
-Below, we present another solution to the readers-writers problem. +
-<code java> +
-/** +
- * This class represents a database.  There are many  +
- * competing threads wishing to read and write.  It is  +
- * acceptable to have multiple processes reading at the  +
- * same time, but if one thread is writing then no other  +
- * process may either read or write. +
- */ +
-public class Database +
-+
-  private int readers; // number of active readers +
-  +
-  /** +
-   * Initializes this database. +
-   */ +
-  public Database() +
-  { +
-    this.readers = 0; +
-  } +
-  +
-  /** +
-   * Read from this database. +
-   */ +
-  public void read(int number) +
-  { +
-    synchronized(this) +
-    { +
-      this.readers++; +
-    } +
-    // read +
-    synchronized(this) +
-    { +
-      this.readers--; +
-      if (this.readers == 0) +
-      { +
-        this.notifyAll(); +
-      } +
-    } +
-  } +
-  +
-  /** +
-   * Writes to this database. +
-   */ +
-  public synchronized void write(int number) +
-  { +
-    while (this.readers != 0) +
-    { +
-      try +
-      { +
-        this.wait(); +
-      } +
-      catch (InterruptedException e) {} +
-    } +
-    // write +
-    this.notifyAll(); +
-  } +
-+
-</code>+
  
 ===== April 2 ===== ===== April 2 =====
Line 368: Line 109:
  
 Examples of JCSP can be found [[csp|here]]. Examples of JCSP can be found [[csp|here]].
-<code java> 
-public class Process implements CSProcess 
-{ 
-  private ChannelOutput verhoog; 
-  private ChannelOutput prolaag; 
- 
-  public Process(ChannelOutput verhoog, ChannelOutput prolaag) 
-  { 
-    super(); 
-    this.verhoog = verhoog; 
-    this.prolaag = prolaag; 
-  } 
- 
-  public void run() 
-  { 
-    this.prolaag.write(null); 
-    // critical section 
-    this.verhoog.write(null); 
-  } 
- 
-</code> 
- 
-<code java> 
-public class Semaphore implements CSProcess 
-{ 
-  private int value; 
-  private AltingChannelInput verhoog; 
-  private AltingChannelInput prolaag; 
- 
-  public Semaphore(int value, AltingChannelInput verhoog, AltingChannelInput prolaag) 
-  { 
-    super(); 
-    this.value = value; 
-    this.verhoog = verhoog; 
-    this.prolaag = prolaag; 
-  } 
- 
-  public void run() 
-  { 
-    final int ALTERNATIVES = 2; 
-    final int V = 0; 
-    final int P = 1; 
-    final Guard[] guard = new Guard[ALTERNATIVES]; 
-    guard[V] = this.verhoog; 
-    guard[P] = this.prolaag; 
-    final boolean[] precondition = new boolean[ALTERNATIVES]; 
-    precondition[V] = true; 
-    final Alternative alternative = new Alternative(guard); 
-    while (true) 
-    { 
-      precondition[P] = this.value > 0; 
-      switch (alternative.select(precondition)) 
-      { 
-        case V: 
-          this.verhoog.read();  
-          this.value++; 
-          break; 
-        case P: 
-          this.prolaag.read();  
-          this.value--; 
-          break; 
-      } 
-    } 
-  } 
-} 
-</code> 
- 
-<code java> 
-public class Main 
-{ 
-  public static void main(String[] args) 
-  { 
-    Any2OneChannel verhoog = Channel.any2one(); 
-    Any2OneChannel prolaag = Channel.any2one(); 
-    Semaphore semaphore = new Semaphore(1, verhoog.in(), prolaag.in()); 
-    Process one = new Process(verhoog.out(), prolaag.out()); 
-    Process two = new Process(verhoog.out(), prolaag.out()); 
-    CSProcess[] process = { semaphore, one, two }; 
-    Parallel parallel = new Parallel(process); 
-    parallel.run(); 
-  } 
-} 
-</code> 
- 
  
 ===== April 16 ===== ===== April 16 =====
Line 487: Line 144:
 Willem Visser, Klaus Havelund, Guillaume Brat, SeungJoon Park and Flavio Lerda. [[http://dx.doi.org/10.1023/A:1022920129859|Model Checking Programs]]. //Automated Software Engineering//, 10(2): 203-232, April 2003.  Willem Visser, Klaus Havelund, Guillaume Brat, SeungJoon Park and Flavio Lerda. [[http://dx.doi.org/10.1023/A:1022920129859|Model Checking Programs]]. //Automated Software Engineering//, 10(2): 203-232, April 2003. 
  
-More information about Java PathFinder can be found  + 
-[[jpf:start|here]].  +
  
 ===== May 7 ===== ===== May 7 =====
 +
 +More information about Java PathFinder can be found 
 +[[jpf:start|here]]. 
  
 ===== May 12 ===== ===== May 12 =====
 +
 +Information about handling native code with Java PathFinder can be found 
 +[[jpf-native:start|here]]. 
  
 ===== May 14 ===== ===== May 14 =====
calendar.1240774731.txt.gz · Last modified: 2009/04/26 19:38 by franck

Donate Powered by PHP Valid HTML5 Valid CSS Driven by DokuWiki