Deprecated: this webpage is preserved for archival purposes. Please consider visiting the new Reo webpage.

Solutions: Instant Messenger

1) Modeling and Verification

  1. Synchronized message receival:

    • Combinations that produce deadlocks:
      • any combination that has at least one EmptyFIFO.

  2. Alternating message receival:

    • Combination that produces deadlocks:
      • if ClientA is set to EmptyFIFO.

  3. Confirmations:

    • The only combination without a deadlock is: ReadOrWrite - ReadOrWrite.

2) Implementation and Execution

The run-method for a client in the EmptyFIFO-mode could look like this:

public void run() {
   try {
      while (true) {
        System.out.println("Waiting for data...");
        String data = in.take();
        System.out.println("Writing data...");
   } catch (InterruptedException e) {

In the FullFIFO-mode, the method should first perform a write and then a take-operation. The ReadOrWrite-mode can be simulated by additionally using timeouts or extra threads.