Scribble parallel loop example

README.md

Scribble parallel loop example

TwoPC1.scr

// Two Producer-Consumer

// Two pairs of a producer and a consumer running in parallel,
// then the two consumers eventually joins in the end.

// The original Scribble accept this (with -fair);
// where two rec's are interpreted as tail recursions,
// which are then composed sequentially.
// In this setting, "continue t;" seems like just a jump (goto),
// not a call, to "rec t {".

module twopc.TwoPC;


global protocol TwoPC(role P1, role P2, role C1, role C2) {
  rec t {
    choice at P1 {
      supply() from P1 to C1;
      continue t;
    } or {
      eos() from P1 to C1;
    }
  }
  rec t2 {
    choice at P2 {
      supply() from P2 to C2;
      continue t2;
    } or {
      eos() from P2 to C2;
    }
  }
  join() from C1 to C2;
}

TwoPC2.scr

module twopc.TwoPC2;
// Scribble rejects this, as there are outputs from non-enabled roles
// whereas (current) nuscr also rejects it, as it is "not mergeable"
// -- due to "unbalanced" branching?
// Currently, I suspect no MPST theory accepts this

global protocol TwoPC2(role P1, role P2, role C1, role C2) {
  rec t {
    choice at P1 {
      supply() from P1 to C1;
      continue t;
    } or {
      eos() from P1 to C1;
      rec t2 {
        choice at P2 {
          supply() from P2 to C2;
          continue t2;
        } or {
          eos() from P2 to C2;
          join() from C1 to C2;
        }
      }
    }
  }
}

TwoPC3.scr

module twopc.TwoPC3;
// TwoPC, in a form of standard global type without sequencing
// This is (perhaps) well-formed in some MPST theory
// e.g. Alceste et al's more "semantic" end point projection --
// see 10.1016/j.jlamp.2018.12.002 
// Scribble rejects this (outputs from non-enabled roles),
// but it is OK (it already accepts TwoPC1)

global protocol TwoPC3(role P1, role P2, role C1, role C2) {
  rec t {
    choice at P1 {
      supply() from P1 to C1;
      choice at P2 {
        supply() from P2 to C2;
        continue t;
      } or {
        eos() from P2 to C2;
        rec t3 {
          choice at P1 {
            supply() from P1 to C1;
            continue t3;
          } or {
            eos() from P1 to C1;
            join from C1 to C2;
          }
        }
      }
    } or {
      eos() from P1 to C1;
      rec t2 {
        choice at P2 {
          supply() from P2 to C2;
          continue t2;
        } or {
          eos() from P2 to C2;
          join() from C1 to C2;
        }
      }
    }
  }
}