PLUG 2020 slides

code/unix-plug2020.links

@@ -0,0 +1,729 @@
+## Prelude
+typename Option(a) = [|None|Some:a|];
+
+sig todo : (String) ~> a
+fun todo(s) { error("TODO: " ^^ s) }
+
+sig fail : () {Fail:Zero |_}-> a
+fun fail() { switch (do Fail) { } }
+
+sig lookup : (a, [(a, b)]) {Fail:Zero |_}~> b
+fun lookup(k, kvs) {
+  switch (kvs) {
+    case [] -> fail()
+    case (k', v) :: kvs' ->
+      if (k == k') v
+      else lookup(k, kvs')
+  }
+}
+
+sig modify : (a, b, [(a, b)]) ~> [(a, b)]
+fun modify(k, v, kvs) {
+  switch (kvs) {
+    case [] -> []
+    case (k', v') :: kvs' ->
+      if (k == k') (k, v) :: kvs'
+      else (k', v') :: modify(k, v, kvs')
+  }
+}
+
+sig remove : (a, [(a, b)]) ~> [(a, b)]
+fun remove(k, kvs) {
+  switch (kvs) {
+    case [] -> []
+    case (k', v') :: kvs' ->
+      if (k == k') kvs'
+      else (k', v') :: remove(k, kvs')
+  }
+}
+
+sig has : (a, [(a, b)]) ~> Bool
+fun has(k, kvs) {
+  switch (kvs) {
+    case [] -> false
+    case (k', _) :: kvs' ->
+      k == k' || has(k, kvs')
+  }
+}
+
+#!
+#
+#        UNIX in 50 lines of code or less
+#               Daniel Hillerström
+#  Laboratory for Foundations of Computer Science
+#          The University of Edinburgh
+#
+#                   PLUG talk
+#             University of Glasgow
+#                December 8, 2020
+#
+#           https://dhil.net/research/
+#
+#?
+
+#!
+#
+# What is an operating system? (very abstractly)
+#
+# A software abstraction that handles a collection of tasks
+#
+# Example tasks:
+#  - Controlling I/O devices
+#  - Scheduling processes
+#  - Signalling errors
+#?
+
+#!
+#
+# What is an effect handler? (very abstractly)
+#
+# An effect handler handles a collection of abstract operations
+#
+# Example operations:
+#  - Reading/writing I/O
+#  - Forking/yielding processes
+#  - Raising exceptions
+#
+#
+#
+#
+#
+#?
+
+#!
+#
+# What is an effect handler? (very abstractly)
+#
+# An effect handler handles a collection of abstract operations
+#
+# Example operations:
+#  - Reading/writing I/O
+#  - Forking/yielding processes
+#  - Raising exceptions
+#
+# Thus an effect handler is an operating system (credit James McKinna)
+# (Kiselyov and Shan (2007) used delimited continuations to model
+#  operating systems)
+#
+#?
+
+#!
+#
+# What is UNIX?
+#
+# UNIX is an operating system designed by Ritchie and Thompson (1974)
+#
+# Components
+#  - Commands (system calls)
+#    + I/O interaction, user session management, inter-process
+#      communication, etc
+#  - Kernel   (interpreter)
+#    + Handling of I/O, managing user sessions, scheduling of
+#      processes
+#  - Development environment
+#    + Compiler tool-chains (e.g. `cc`)
+#  - Documentation
+#    + manual pages (e.g. `man`)
+#
+#?
+
+#!
+#
+# Key characteristics of a UNIX-y operating system
+#
+# - Support for multiple user sessions
+# - Time-sharing between processes
+# - "Everything is a file"
+#
+#?
+
+#!
+#
+# Basic I/O: Performing writes
+#
+typename File = String;
+typename FileDescr = Int;
+
+sig stdout : FileDescr
+var stdout = 1;
+
+sig echo : (String) {Write:(FileDescr,String) -> () |%}-> ()
+fun echo(cs) { todo("echo") }
+#?
+
+#!
+#
+# Basic I/O: Handling writes
+#
+sig basicIO : ( () {Write:(FileDescr,String) -> () |%}-> a ) { |%}-> (a, File)
+fun basicIO(m) {
+    todo("implement basicIO")
+}
+#?
+
+#!
+#
+# Basic I/O: Example
+#
+sig example0 : () { |%}-> ((), File)
+fun example0() {
+  basicIO(fun() {
+        echo("Hello"); echo("World")
+  })
+}
+#?
+
+#!
+#
+# Dynamic semantics of handlers
+#
+#  (ret) handle(V) { case Return(x) -> N case ... }
+#        ~> N[V/x]
+#
+#  (op)  handle(E[do Op(V)]) { case Op(p,r) -> N case ... }
+#        ~> N[V/p
+#            ,fun(x){ handle(E[x]) { case Op(p,r) -> N case ... }}/r]
+#        (if Op \notin E)
+#
+#?
+
+#!
+#
+# Exceptions: Premature exits
+#
+sig exit : (Int) {Exit:(Int) -> Zero |%}-> a
+fun exit(n) { todo("implement exit") }
+#?
+
+#!
+#
+# Handling exits
+#
+sig status : (() {Exit:(Int) -> Zero |%}-> a) { |%}-> Int
+fun status(m) {
+  todo("implement status")
+}
+#?
+
+#!
+#
+# Handling exits: Example
+#
+sig example1 : () { |%}-> (Int, File)
+fun example1() {
+  basicIO(fun() {
+        status(fun() {
+          echo("dead"); exit(1); echo("code")
+        })
+  })
+}
+#?
+
+#!
+#
+# Dynamic binding: User-specific environments (1)
+#
+typename User = [|Alice|Bob|Root|];
+
+sig whoami : () {Ask:String |%}-> String
+fun whoami() { do Ask }
+#?
+
+#!
+#
+# Dynamic binding: User-specific environments (2)
+#
+sig env : (User, () {Ask:String |%}-> a) { |%}-> a
+fun env(user, m) {
+  handle(m()) {
+    case Return(x) -> x
+    case Ask(resume) ->
+      switch (user) {
+        case Alice -> resume("alice")
+        case Bob   -> resume("bob")
+        case Root  -> resume("root")
+      }
+  }
+}
+
+
+sig example2 : () { |%}-> String
+fun example2() {
+  env(Root, whoami)
+}
+#?
+
+#!
+#
+# Aside: Dynamic binding with delimited continuations
+#
+# The idea of dynamic binding dates back to at least McCarthy (1960)
+#
+# Kiselyov, Shan, and Sabry (2006) demonstrated dynamic binding can be
+# simulated with delimited continuations
+#
+#?
+
+#!
+#
+# User session management
+#
+sig su : (User) {Su:(User) -> () |%}-> ()
+fun su(user) { do Su(user) }
+
+sig sessionmgr : (User, () {Ask:String, Su:(User) -> () |%}-> a) { |%}-> a
+fun sessionmgr(user, m) {
+  env(user, fun() {
+     handle(m()) {
+       case Return(x) -> x
+       case Su(user', resume) ->
+         env(user', fun() { resume(()) })
+     }
+  })
+}
+#?
+
+#!
+#
+# Multiple user sessions example
+#
+sig example3 : () { |%}-> (Int, File)
+fun example3() {
+  basicIO(fun() {
+        sessionmgr(Root, fun() {
+          status(fun() {
+            su(Alice); echo(whoami()); echo(" ");
+            su(Bob);   echo(whoami()); echo(" ");
+            su(Root);  echo(whoami())
+          })
+        })
+  })
+}
+#?
+
+#!
+#
+# Nondeterminism: Multi-tasking
+#
+sig fork : () {Fork:Bool |_}-> Bool
+fun fork() { do Fork }
+
+sig nondet : (() {Fork:Bool |%}-> a) { |%}-> [a]
+fun nondet(m) {
+  handle(m()) {
+    case Return(res)  -> todo("implement nondet Return case")
+    case Fork(resume) -> todo("implement nondet Fork case")
+  }
+}
+#?
+
+#!
+#
+# Nondeterminism: Example (1)
+#
+sig ritchie : () {Write:(FileDescr, String) -> () |%}-> ()
+fun ritchie() {
+  echo("UNIX is basically ");
+  echo("a simple operating system, ");
+  echo("but ");
+  echo("you have to be a genius to understand the simplicity.\n")
+}
+
+sig hamlet : () {Write:(FileDescr, String) -> () |%}-> ()
+fun hamlet() {
+  echo("To be, or not to be,\n");
+  echo("that is the question:\n");
+  echo("Whether 'tis nobler in the mind to suffer\n")
+}
+#?
+
+#!
+#
+# Nondeterminism: Example (2)
+#
+sig example4 : () { |%}-> ([Int], File)
+fun example4() {
+  basicIO(fun() {
+    nondet(fun() {
+      sessionmgr(Root, fun() {
+        status(fun() {
+          if (fork()) {
+            su(Alice);
+            ritchie()
+          } else {
+            su(Bob);
+            hamlet()
+          }
+        })
+      })
+    })
+  })
+}
+#?
+
+#
+#
+# Mathematically well-founded nondeterminism
+#
+# The handler `nondet` is _exactly_ the handler Plotkin and Pretnar (2013)
+# give for nondeterminism
+# It satisfies the usual (semi-lattice) equations for nondeterministic choice, i.e.
+#
+#   if (fork()) M else M                        = M
+#   if (fork()) M else N                        = if (fork()) N else M
+#   if (fork()) L else { if (fork()) M else N } = if (fork()) { if (fork()) L else M } else N
+#
+#
+
+#!
+#
+# Interrupting processes
+#
+sig interrupt : () {Interrupt:() |%}-> ()
+fun interrupt() { do Interrupt }
+
+# Process reification
+typename Pstate(a,e::Eff)
+         = forall q::Presence.
+           [|Done:a
+            |Paused:() {Interrupt{q} |e}-> Pstate(a, { |e})|];
+
+
+sig reifyProcess : (() {Interrupt:() |%}-> a) { |%}-> Pstate(a, { |%})
+fun reifyProcess(m) {
+  handle(m()) {
+    case Return(res) -> Done(res)
+    case Interrupt(resume) -> Paused(fun() { resume(()) })
+  }
+}
+#?
+
+#!
+#
+# Time-sharing via interrupts
+#
+sig schedule : ([Pstate(a, { Fork:Bool |%})]) { |%}~> [a]
+fun schedule(ps) {
+  fun schedule(ps, done) {
+    switch (ps) {
+      case [] -> done
+      case Done(res) :: ps' ->
+        schedule(ps', res :: done)
+      case Paused(resume) :: ps' ->
+        schedule(ps' ++ nondet(resume), done)
+    }
+  }
+  schedule(ps, [])
+}
+
+sig timeshare : (() {Fork:Bool,Interrupt:() |%}-> a) { |%}-> [a]
+fun timeshare(m) {
+  var p = Paused(fun() { reifyProcess(m) });
+  schedule([p])
+}
+#?
+
+#!
+#
+# Injecting interrupts
+#
+# First idea: external source injects interrupts (Ahman and Pretnar (2021))
+#
+# Second idea: bundle interrupts with other operations
+sig echo' : (FileDescr,String) {Interrupt:(), Write:(FileDescr,String) -> () |%}-> ()
+fun echo'(fd, cs) { interrupt(); do Write(fd, cs) }
+#
+# Third idea: overload interpretations of operations
+sig interruptWrite : (() {Write:(FileDescr,String) -> () |%}-> a) {Write:(FileDescr,String) -> () |%}-> a
+fun interruptWrite(m) {
+  handle(m()) {
+    case Return(res) -> res
+    case Write(fd, cs, resume) ->
+      interrupt(); resume(do Write(fd, cs))
+  }
+}
+#?
+
+#!
+#
+# Time-sharing example
+#
+sig example5 : () { |%}-> ([Int], File)
+fun example5() {
+  basicIO(fun() {
+    timeshare(fun() {
+      interruptWrite(fun() {
+        sessionmgr(Root, fun() {
+          status(fun() {
+            if (fork()) {
+              su(Alice);
+              ritchie()
+            } else {
+              su(Bob);
+              hamlet()
+            }
+          })
+        })
+      })
+    })
+  })
+}
+#?
+
+#!
+#
+# State: File I/O
+#
+# Generic state handling
+sig get : () {Get:s |_}-> s
+fun get() { do Get }
+
+sig put : (s) {Put:(s) -> () |_}-> ()
+fun put(st) { do Put(st) }
+
+sig runState : (s, () {Get:() -> s,Put:(s) -> () |%}-> a) { |%}-> (a, s)
+fun runState(st0, m) {
+  var f = handle(m()) {
+    case Return(x)       -> fun(st) { (x, st) }
+    case Get(resume)     -> fun(st) { resume(st)(st) }
+    case Put(st',resume) -> fun(_)  { resume(())(st') }
+  };
+  f(st0)
+}
+#?
+
+#!
+#
+# Basic Serial File System
+#
+#     Directory              I-List              Data region
+# +----------------+        +-------+     +--------------------------+
+# | "hamlet"       |------> |   2   |---> | "To be, or not to be..." |
+# +----------------+     /  +-------+     +--------------------------+
+# | "richtie.txt"  |------> |   1   |---> | "UNIX is basically..."   |
+# +----------------+    /   +-------+     +--------------------------+
+# | ...            |    |   |  ...  |     | ...                      |
+# +----------------+    |   +-------+     +--------------------------+
+# | "stdout"       |------> |   1   |---> | ""                       |
+# +----------------+    |   +-------+     +--------------------------+
+# | ...            |    /
+# +----------------+   /
+# | "act3"         |---
+# +----------------+
+#
+# Simplifications:
+#   - Operating directly on inode pointers
+#   - Reads and writes will be serial
+#
+#?
+
+#!
+#
+# BSFS structures
+#
+typename INode      = (loc:Int,lno:Int);
+typename IList      = [(Int, INode)];  # INode index -> INode
+typename Directory  = [(String, Int)]; # Filename -> INode index
+typename DataRegion = [(Int, File)];   # Loc -> File
+
+typename FileSystem = (dir:Directory,dregion:DataRegion,inodes:IList
+                                    ,lnext:Int         ,inext:Int    );
+
+sig fsys0 : FileSystem
+var fsys0 = ( dir     = [("stdout", 0)]
+            , inodes  = [(0, (loc=0, lno=1))]
+            , dregion = [(0, "")]
+            , lnext = 1, inext = 1 );
+#?
+
+#!
+#
+# Utility functions
+#
+sig lookup : (a, [(a, b)]) {Fail:Zero |%}-> b
+var lookup = lookup;
+
+sig modify : (a, b, [(a, b)]) { |%}-> [(a, b)]
+var modify = modify;
+
+sig remove : (a, [(a, b)]) { |%}-> [(a, b)]
+var remove = remove;
+
+sig has : (a, [(a, b)]) { |%}-> Bool
+var has = has;
+
+sig withDefault : (a, () {Fail:Zero |%}-> a) { |%}-> a
+fun withDefault(x', m) {
+  handle(m()) {
+    case Return(x) -> x
+    case Fail(_)   -> x'
+  }
+}
+#?
+
+#!
+#
+# BSFS primitive operations: file reading and writing
+#
+sig fwrite : (Int, String, FileSystem) {Fail:Zero |%}-> FileSystem
+fun fwrite(ino, cs, fsys) {
+  var inode = lookup(ino, fsys.inodes);
+  var file  = lookup(inode.loc, fsys.dregion);
+  var file' = file ^^ cs;
+  (fsys with dregion = modify(inode.loc, file', fsys.dregion))
+}
+
+sig fread : (Int, FileSystem) {Fail:Zero |%}-> String
+fun fread(ino, fsys) {
+  var inode = lookup(ino, fsys.inodes);
+  lookup(inode.loc, fsys.dregion)
+}
+#?
+
+#!
+#
+# Handling reading and writing
+#
+sig fileRW : ( () { Read :(FileDescr) -> Option(String)
+                  , Write:(FileDescr, String) -> ()     |%}-> a )
+                          {Get:FileSystem,Put:(FileSystem) -> () |%}-> a
+fun fileRW(m) {
+  handle(m()) {
+    case Return(ans) -> ans
+    case Read(fd, resume) ->
+      var cs = withDefault(None, fun() {
+                 Some(fread(fd, get()))
+               });
+      resume(cs)
+    case Write(fd, cs, resume) ->
+      withDefault((), fun() {
+        var fsys = fwrite(fd, cs, get());
+        put(fsys)
+      }); resume(())
+  }
+}
+#?
+
+#!
+#
+# BSFS operation: file opening and creation
+#
+sig fopen : (String, FileSystem) {Fail:Zero |%}-> FileDescr
+fun fopen(fname, fsys) { lookup(fname, fsys.dir) }
+
+sig fcreate : (String, FileSystem) {Fail:Zero |%}-> (FileDescr, FileSystem)
+fun fcreate(fname, fsys) {
+  if (has(fname, fsys.dir)) {
+    var ino = fopen(fname, fsys);
+    # Truncate file
+    var inode = lookup(ino, fsys.inodes);
+    var dregion = modify(inode.loc, "", fsys.dregion);
+    (ino, (fsys with =dregion))
+  } else {
+    var loc = fsys.lnext;
+    var dregion = (loc, "") :: fsys.dregion;
+
+    var ino   = fsys.inext;
+    var inode = (loc=loc,lno=1);
+    var inodes = (ino, inode) :: fsys.inodes;
+
+    var dir = (fname, ino) :: fsys.dir;
+    (ino, (=dir, =dregion, =inodes, lnext=loc+1, inext=ino+1))
+  }
+}
+#?
+
+#!
+#
+# Handling file creation and opening
+#
+sig fileOC : ( () { Open  :(String) -> Option(FileDescr)
+                  , Create:(String) -> Option(FileDescr) |%}-> a )
+                          {Get:FileSystem,Put:(FileSystem) -> () |%}-> a
+fun fileOC(m) {
+  handle(m()) {
+    case Return(ans) -> ans
+    case Open(fname, resume) ->
+      var fd = withDefault(None, fun() {
+                 Some(fopen(fname, get()))
+               }); resume(fd)
+    case Create(fname, resume) ->
+      var fd = withDefault(None, fun() {
+                 var (fd, fsys) = fcreate(fname, get());
+                 put(fsys); Some(fd)
+               }); resume(fd)
+  }
+}
+#?
+
+#!
+#
+# BSFS version 0
+#
+sig bsfs0 : ( () {  Open  :(String) -> Option(FileDescr)
+                  , Create:(String) -> Option(FileDescr)
+                  , Read :(FileDescr) -> Option(String)
+                  , Write:(FileDescr, String) -> ()     |%}-> a )
+                          {Get:FileSystem,Put:(FileSystem) -> () |%}-> a
+fun bsfs0(m) {
+  fileOC(fun() {
+    fileRW(m)
+  })
+}
+#?
+
+#!
+#
+# Stream redirection
+#
+sig >- : (() { |%}-> a, String)
+                { Create:(String) -> Option(FileDescr)
+                , Exit  : (Int) -> Zero
+                , Write :(FileDescr,String) -> ()      |%}-> a
+op f >- fname {
+  var fd = switch (do Create(fname)) {
+             case None -> exit(-1)
+             case Some(fd) -> fd
+  }; handle(f()) {
+      case Return(x) -> x
+      case Write(_, cs, resume) ->
+       resume(do Write(fd, cs))
+    }
+}
+#?
+
+#!
+#
+# Plugging everything together
+#
+sig example6 : (FileSystem) { |%}-> ([Int], FileSystem)
+fun example6(fsys) {
+  runState(fsys, fun() {
+    bsfs0(fun() {
+      timeshare(fun() {
+        sessionmgr(Root, fun() {
+          status(fun() {
+            if (fork()) {
+              su(Alice);
+              ritchie >- "ritchie.txt"
+            } else {
+              su(Bob);
+              hamlet >- "hamlet"
+            }
+          })
+        })
+      })
+    })
+  })
+}
+#?
+
+#!
+#
+# Conclusion
+#
+# Effect handlers are a versatile programming abstraction
+# Operating systems can be explained in terms of handlers
+# "Every problem can be solved by adding another handler"
+#
+#?