## 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) # # An operating system responds to a collection of system calls # # Example tasks: # - Signalling errors # - Scheduling processes # - Reading/writing I/O #? #! # # What is an effect handler? (very abstractly) # # An effect handler responds a collection of abstract operation calls # # Example tasks: # - Signalling errors # - Scheduling processes # - Reading/writing I/O # # # # # #? #! # # What is an effect handler? (very abstractly) # # An effect handler responds a collection of abstract operation calls # # Example tasks: # - Signalling errors # - Scheduling processes # - Reading/writing I/O # # Thus an effect handler is an operating system (credit James McKinna) # (Kiselyov and Shan (2007) used delimited continuations to model # operating systems) # #? #! # # Objectives of this talk # # - Demonstrate the versatility of handlers # - Explain operating systems as the combination of # + Exceptions # + Dynamic binding # + Nondeterminism # + State # #? # # # 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 UNIX (Ritchie & Thompson, 1974) # # - 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("implement 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 (1) # # From the man pages. # # Description # fork() creates a new process by duplicating the calling process. The # new process is referred to as the child process. The calling process # is referred to as the parent process. # # Return value # On success, the PID of the child process is returned in the parent, # and 0 is returned in the child. # #? #! # # Nondeterminism: Multi-tasking (2) # sig fork : () {Fork:Bool |_}-> Bool fun fork() { do Fork } sig nondet : (() {Fork:Bool |%}-> a) { |%}-> [a] fun nondet(m) { handle(m()) { case Return(ans) -> todo("implement Return case") case Fork(resume) -> todo("implement 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(ans) -> Done(ans) 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) } #? #! # # State: Example # sig incr : () {Get:Int,Put:(Int) -> () |%}-> () fun incr() { put(get() + 1) } sig example6 : () { |%}-> ((), Int) fun example6() { runState(41, incr) } #? #! # # 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 withDefault : (a, () {Fail:Zero |%}-> a) { |%}-> a fun withDefault(x', m) { handle(m()) { case Return(x) -> x case Fail(_) -> x' } } #? 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 BSFS operations: file reading and writing # sig fwrite : (FileDescr, String, FileSystem) {Fail:Zero |%}-> FileSystem var fwrite = fwrite; sig fread : (FileDescr, FileSystem) {Fail:Zero |%}-> String var fread = fread; 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(()) } } #? 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)) } } #! # # BSFS operation: file opening and creation # sig fopen : (String, FileSystem) {Fail:Zero |%}-> FileDescr var fopen = fopen; sig fcreate : (String, FileSystem) {Fail:Zero |%}-> (FileDescr, FileSystem) var fcreate = fcreate; 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)) } } #? #! # # Crude copy # sig ccp : (String, String) { Create:(String) -> Option(FileDescr) , Exit :(Int) -> Zero , Read :(FileDescr) -> Option(String) , Open :(String) -> Option(FileDescr) , Write :(FileDescr,String) -> () |%}-> () fun ccp(src, dst) { var srcfd = switch (do Open(src)) { case None -> exit(-1) case Some(fd) -> fd }; switch (do Read(srcfd)) { case None -> exit(-1) case Some(cs) -> fun() {echo(cs)} >- dst } } #? #! # # Plugging everything together # sig example7 : () { |%}-> ([Int], FileSystem) fun example7() { runState(fsys0, fun() { bsfs0(fun() { timeshare(fun() { sessionmgr(Root, fun() { status(fun() { if (fork()) { su(Alice); ritchie >- "ritchie.txt" } else { su(Bob); hamlet >- "hamlet"; ccp("hamlet", "act3") } }) }) }) }) }) } #? #! # # 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" # #?