Notes on Scribble

Demos and examples

• FASE'16 paper Hybrid Session Verification through Endpoint API Generation

  • Adder and SMTP (code)

• FASE'17 paper Explicit Connection Actions in Multiparty Session Types

  • Scribble source with "explicit connection"
  • Travel Agency 2 with "explicit connection" and "binary connection correlation"
  • Microservices use case in Appendix D

• BETTY Summer School 2016

  • Lecture 1 PDF
    • HTTP (short and long), OOI Agent negotiation (nego), and various exercises (misc)
  • Lecture 2 PDF
    • Adder (and its Fibonacci client), SMTP and OOI Resource Usage Control (interruptible)
  • Scribble source code
  • Scribble source for "interruptible" (from POPL'14 tutorial, in scribble-python)
    • Play-Resume pattern, a page with figures in OOI website
    • Original paper on interruptible (FMSD'15)

• Other examples on "interruptible" and "parallel composition" (par)

  • Scribble source

• Others

  • Game with delegation from A Linear Decomposition of Multiparty Sessions (ECOOP'17) paper and artifact
  • Three Buyer Protocol, dynamically interleaved sessions from MSCS'16 paper
  • LoanApplication
  • Remote Procedure Call
  • Travel agency
  • Java RMI (remote method invocation)

Scribble-OCaml status

• booking.ml (generated API) and booking_example.ml (user code)

• explicit connection (API) and example code

• OCaml code generated from FASE'16

• OCaml code generated from FASE'17

• others

• Worked (i.e., .ml is generated)

  • fase16 adder and smtp
  • MathService
  • LoanApplication
  • RPCComp, RPCComp2, MyRelay in RPC.scr
  • TwoBuyer, TwoBuyerChoice, Proto in ThreeBuyer.scr
  • Booking in Travel.scr
  • BookingExp in Travel.scr
  • Travel2.scr in FASE'17
  • "OptionalDynamicThirdParty" and "P2" in fase17/Sec1.scr

• Doesn't work

  • Game1.scr and Game2.scr
  • Because of delegation on external choice

• Didn't work for other reason

  • "AppD.scr" in fase17/AppD.scr

Features

• Explicit connection and binary connection correlation (above)
• Delegation (above)
• Interruption (above)
• Multiparty Protocol Induced Recovery (CC'17) and its implementation
• Timed features (delay?) Timed Multiparty Session Types (CONCUR'14) and its implementation
• Parameterised (Pabble) https://github.com/pabble-lang/pabble-mpi Protocols by Default: Safe MPI Code Generation based on Session Types (CC'15)