From 604e8047f1620f104f6f44bb4c7e788ddf93f17d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Mon, 26 Oct 2020 23:26:46 +0000 Subject: [PATCH] Update code --- code/unix2.links | 281 +++++++++++++++++++++++++++++++---------------- 1 file changed, 187 insertions(+), 94 deletions(-) diff --git a/code/unix2.links b/code/unix2.links index ae8277a..9d5509f 100644 --- a/code/unix2.links +++ b/code/unix2.links @@ -1,16 +1,32 @@ # Tiny UNIX revision 2. -sig str : ((a, [Char])) ~> (a, String) -fun str((x, cs)) { (x, implode(cs)) } - typename Option(a) = [|None|Some:a|]; -sig lookup : (a, [(a, b)]) ~> Option(b) +sig fail : () {Fail:Zero |_}-> a +fun fail() { switch (do Fail) {} } + +sig optionalise : (Comp(a, {Fail:Zero |e})) {Fail{_} |e}~> Option(a) +fun optionalise(m) { + handle(m()) { + case Return(x) -> Some(x) + case Fail(_) -> None + } +} + +sig withDefault : (a, Comp(a, {Fail:Zero |e})) {Fail{_} |e}~> a +fun withDefault(x', m) { + handle(m()) { + case Return(x) -> x + case Fail(_) -> x' + } +} + +sig lookup : (a, [(a, b)]) {Fail:Zero |_}~> b fun lookup(k, kvs) { switch (kvs) { - case [] -> None + case [] -> fail() case (k', v) :: kvs' -> - if (k == k') Some(v) + if (k == k') v else lookup(k, kvs') } } @@ -44,14 +60,6 @@ fun has(k, kvs) { } } -sig fromSome : (Option(a)) ~> a -fun fromSome(x) { - switch (x) { - case None -> error("fromSome") - case Some(x) -> x - } -} - ## ## Basic i/o ## @@ -185,22 +193,32 @@ fun slice(m) { } } -sig runNext : ([Pstate(a, { Fork:Bool |e})]) {Fork{_},Interrupt{_} |e}~> [a] -fun runNext(ps) { - sig run : (Pstate (a, { Fork:() {}-> Bool|e })) {Fork{_},Interrupt{_} |e}~> [a] - fun run(p) { - switch(p) { - case Done(res) -> [res] - case Paused(resume) -> runNext(nondet(resume)) +sig schedule : ([Pstate(a, { Fork:Bool |e})]) {Fork{_},Interrupt{_} |e}~> [a] +fun schedule(ps) { + # sig run : (Pstate (a, { Fork:() {}-> Bool|e })) {Fork{_},Interrupt{_} |e}~> [a] + # fun run(p) { + # switch(p) { + # case Done(res) -> [res] + # case Paused(resume) -> runNext(nondet(resume)) + # } + # } + # concatMap(run, 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) } } - concatMap(run, ps) + schedule(ps, []) } sig timeshare : (Comp(a, {Fork:Bool,Interrupt:() |e})) {Fork{_},Interrupt{_} |e}~> [a] fun timeshare(m) { var p = Paused(fun() { slice(m) }); - runNext([p]) + schedule([p]) } fun example4() { @@ -231,6 +249,89 @@ fun example4() { }) } +fun forktest(n) { + fun loop(i, n) { + if (i >= n) (-1) + else { + var x = fork(); + println("< x = " ^^ (if (x) "true" else "false") ^^ ", i = " ^^ intToString(i)); + ignore(loop(i+1,n)); + println("> x = " ^^ (if (x) "true" else "false") ^^ ", i = " ^^ intToString(i)); + exit(i) + } + } + loop(0, n) +} + +fun test(i) { + if (i == 2) () + else { + println("< i = " ^^ intToString(i)); + var x = fork(); + test(i+1); + println("> i = " ^^ intToString(i)) + } +} + +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") +} + +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") +} + +fun example5() { + basicIO(fun() { + nondet(fun() { + sessionmgr(Root, fun() { + status(fun() { + if (fork()) { + su(Alice); + ritchie() + } else { + su(Bob); + hamlet() + } + }) + }) + }) + }) +} + +fun interruptWrite(m) { + handle(m()) { + case Return(res) -> res + case Write(fd, cs, resume) -> + interrupt(); resume(do Write(fd, cs)) + } +} + +fun example5'() { + basicIO(fun() { + timeshare(fun() { + interruptWrite(fun() { + sessionmgr(Root, fun() { + status(fun() { + if (fork()) { + su(Alice); + ritchie() + } else { + su(Bob); + hamlet() + } + }) + }) + }) + }) + }) +} + ## ## Generic state handling ## @@ -250,7 +351,7 @@ fun runState(st0, m) { f(st0) } -fun example5() { +fun example6() { runState(0, fun() { var x = 3; put(x); @@ -280,21 +381,20 @@ typename FileSystem = (dir:Directory,dregion:DataRegion,inodes:IList sig fsys0 : FileSystem var fsys0 = (dir = [("stdout", 0)], inodes = [(0, (loc=0, lno=1))], dregion = [(0, "")], lnext = 1, inext = 1); -sig fopen : (String, FileSystem) ~> (Option(Int), FileSystem) +sig fopen : (String, FileSystem) {Fail:Zero |_}~> (Int, FileSystem) fun fopen(fname, fsys) { (lookup(fname, fsys.dir), fsys) } -sig ftruncate : (Int, FileSystem) ~> FileSystem +sig ftruncate : (Int, FileSystem) {Fail:Zero |_}~> FileSystem fun ftruncate(ino, fsys) { - var inode = fromSome(lookup(ino, fsys.inodes)); + var inode = lookup(ino, fsys.inodes); var dregion = modify(inode.loc, "", fsys.dregion); (fsys with =dregion) } -sig fcreate : (String, FileSystem) ~> (Int, FileSystem) +sig fcreate : (String, FileSystem) {Fail:Zero |_}~> (Int, FileSystem) fun fcreate(fname, fsys) { if (has(fname, fsys.dir)) { var (ino, fsys) = fopen(fname, fsys); - var ino = fromSome(ino); (ino, ftruncate(ino, fsys)) } else { var loc = fsys.lnext; @@ -309,65 +409,59 @@ fun fcreate(fname, fsys) { } } -sig ftruncate : (Int, FileSystem) ~> FileSystem +sig ftruncate : (Int, FileSystem) {Fail:Zero |_}~> FileSystem fun ftruncate(ino, fsys) { - var inode = fromSome(lookup(ino, fsys.inodes)); + var inode = lookup(ino, fsys.inodes); var dregion = modify(inode.loc, "", fsys.dregion); (fsys with =dregion) } -sig fopen : (String, FileSystem) ~> (Option(Int), FileSystem) -fun fopen(fname, fsys) { (lookup(fname, fsys.dir), fsys) } +sig fopen : (String, FileSystem) {Fail:Zero |_}~> Int +fun fopen(fname, fsys) { lookup(fname, fsys.dir) } sig fclose : (Int, FileSystem) ~> FileSystem fun fclose(_, fsys) { fsys } -sig fwrite : (Int, String, FileSystem) ~> FileSystem +sig fwrite : (Int, String, FileSystem) {Fail:Zero |_}~> FileSystem fun fwrite(ino, cs, fsys) { - var inode = fromSome(lookup(ino, fsys.inodes)); - var file = fromSome(lookup(inode.loc, fsys.dregion)); + 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) ~> Option(String) +sig fread : (Int, FileSystem) {Fail:Zero |_}~> String fun fread(ino, fsys) { - var inode = fromSome(lookup(ino, fsys.inodes)); + var inode = lookup(ino, fsys.inodes); lookup(inode.loc, fsys.dregion) } -sig flink : (String, String, FileSystem) ~> Option(FileSystem) +sig flink : (String, String, FileSystem) {Fail:Zero |_}~> FileSystem fun flink(src, dest, fsys) { - switch (lookup(dest, fsys.dir)) { - case None -> None - case Some(ino) -> - var inode = fromSome(lookup(ino, fsys.inodes)); - var inode = (inode with lno = inode.lno + 1); - var inodes = modify(ino, inode, fsys.inodes); - - var dir = (src, ino) :: fsys.dir; - Some((fsys with inodes = inodes, dir = dir)) - } + var ino = lookup(dest, fsys.dir); + var inode = lookup(ino, fsys.inodes); + var inode' = (inode with lno = inode.lno + 1); + var inodes = modify(ino, inode', fsys.inodes); + + var dir = (src, ino) :: fsys.dir; + (fsys with inodes = inodes, dir = dir) } -sig funlink : (String, FileSystem) ~> Option(FileSystem) +sig funlink : (String, FileSystem) {Fail:Zero |_}~> FileSystem fun funlink(fname, fsys) { - switch (lookup(fname, fsys.dir)) { - case None -> None - case Some(i) -> - var dir = remove(fname, fsys.dir); - - var inode = fromSome(lookup(i, fsys.inodes)); - var inode = (inode with lno = inode.lno - 1); - - if (inode.lno > 0) { - var inodes = modify(i, inode, fsys.inodes); - Some((fsys with inodes = inodes, dir = dir)) - } else { - var dregion = remove(inode.loc, fsys.dregion); - var inodes = remove(i, fsys.inodes); - Some((fsys with inodes = inodes, dir = dir, dregion = dregion)) - } + var i = lookup(fname, fsys.dir); + var dir = remove(fname, fsys.dir); + + var inode = lookup(i, fsys.inodes); + var inode' = (inode with lno = inode.lno - 1); + + if (inode'.lno > 0) { + var inodes = modify(i, inode', fsys.inodes); + (fsys with inodes = inodes, dir = dir) + } else { + var dregion = remove(inode'.loc, fsys.dregion); + var inodes = remove(i, fsys.inodes); + (fsys with inodes = inodes, dir = dir, dregion = dregion) } } @@ -398,32 +492,38 @@ fun unlink(fname) { do Unlink(fname) } sig injectState : (() { |e}~> a) -> () {Get:s,Put:(s) -> () |e}~> a fun injectState(f) { (f : (() {Get:s,Put:(s) -> () |e}~> a) <- (() { |e}~> a)) } -sig fileIO : (Comp(a, { Close:(FileDescr) -> () - , Create:(String) -> FileDescr +sig fileIO : (Comp(a, { #Close:(FileDescr) -> () + Create:(String) -> FileDescr , Read:(FileDescr) -> Option(String) , Open:(String) -> Option(FileDescr) , Truncate:(FileDescr) -> () - , Write:(FileDescr, String) -> () |e})) - {Close{_},Create{_},Read{_},Open{_},Truncate{_},Write{_},Get:FileSystem,Put:(FileSystem) -> () |e}~> a + , Write:(FileDescr, String) -> () + , Fail{p}|e})) + {Create{_},Read{_},Open{_},Truncate{_},Write{_},Get:FileSystem,Put:(FileSystem) -> (),Fail{p} |e}~> a fun fileIO(m) { handle(injectState(m)()) { case Return(x) -> x - case Close(_, resume) -> - resume(()) case Create(fname, resume) -> - var (fd, fsys) = fcreate(fname, get()); - put(fsys); resume(fd) - case Read(fd, resume) -> - resume(fread(fd, get())) + var ino = withDefault(-1, fun() { + var (ino, fsys) = fcreate(fname, get()); + put(fsys); ino + }); resume(ino) + case Read(ino, resume) -> + var contents = optionalise(fun() { fread(ino, get()) }); + resume(contents) case Open(fname, resume) -> - var (fd, fsys) = fopen(fname, get()); - put(fsys); resume(fd) - case Truncate(fd, resume) -> - var fsys = ftruncate(fd, get()); - put(fsys); resume(()) - case Write(fd, cs, resume) -> - var fsys = fwrite(fd, cs, get()); - put(fsys); resume(()) + var ino = optionalise(fun() { fopen(fname, get()) }); + resume(ino) + case Truncate(ino, resume) -> + withDefault((), fun() { + var fsys = ftruncate(ino, get()); + put(fsys) + }); resume(()) + case Write(ino, cs, resume) -> + withDefault((), fun() { + var fsys = fwrite(ino, cs, get()); + put(fsys) + }); resume(()) } } @@ -477,20 +577,13 @@ op f >>> fname { } } -fun example6() { +fun example7() { if (fork()) { su(Alice); - var fd = create("ritchie.txt"); - fun(){echo("UNIX is basically a simple operating system, ")} >> "ritchie.txt"; - fun(){echo("but you have to be a genius to understand the simplicity.")} >>> "ritchie.txt" + ritchie >> "ritchie.txt" } else { su(Bob); - var hamlet = "hamlet"; - fun(){echo("To be, or not to be, that is the question:\n")} >> hamlet; - fun(){echo("Whether 'tis nobler in the mind to suffer\n")} >>> hamlet; - fun(){echo("The slings and arrows of outrageous fortune,\n")} >>> hamlet; - fun(){echo("Or to take arms against a sea of troubles\n")} >>> hamlet; - fun(){echo("And by opposing end them.")} >>> hamlet + hamlet >> "hamlet" } }