From d6a83c244237ee0c5408e33354d1428ebdf513c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Tue, 8 Dec 2020 00:06:11 +0000 Subject: [PATCH] PLUG 2020 slides --- code/unix-plug2020.links | 729 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 729 insertions(+) create mode 100644 code/unix-plug2020.links diff --git a/code/unix-plug2020.links b/code/unix-plug2020.links new file mode 100644 index 0000000..f9fc882 --- /dev/null +++ b/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" +# +#?