Created
February 13, 2018 14:13
-
-
Save prepor/b214eac430f2fa8de54b3550f090b584 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module OAM-SYNTAX | |
| syntax Ints ::= List{Int,","} | |
| syntax Op ::= "#parallel" Int Int | |
| | "#otherwise" Int Int | |
| | "#pruning" Int Int Int | |
| | "#sequential" Int Int Int | |
| | "#callFun" Int "[" Ints "]" | |
| | "#callDynamic" Int "[" Ints "]" | |
| | "#ffi" Int "[" Ints "]" | |
| | "#coeffect" Int | |
| | "#stop" | |
| | "#constInt" Int | |
| | "#closure" Int Int | |
| | "#label" Int | |
| syntax Val ::= Int | |
| syntax SourceOp ::= Int ":" Op | |
| syntax SourceOps ::= List{SourceOp, " "} | |
| syntax SourceFun ::= Int Int "{" SourceOps "}" | |
| syntax SourceFuns ::= List{SourceFun, " "} | |
| syntax SourceFFI ::= Int String | |
| syntax SourceFFIs ::= List{SourceFFI, " "} | |
| syntax Source ::= "ffi" "{" SourceFFIs "}" SourceFuns | |
| endmodule | |
| module OAM | |
| imports OAM-SYNTAX | |
| syntax Stack ::= stack(List) | |
| syntax List ::= #reverseList(List, List) [function] | |
| rule #reverseList(Res, .List) => Res | |
| rule #reverseList((.List => ListItem(I)) _, (ListItem(I) => .List) _) | |
| syntax Stack ::= #incrementInstances(List, List) [function] | |
| rule #incrementInstances(Acc, .List) => stack(#reverseList(.List, Acc)) | |
| rule #incrementInstances(Acc, | |
| (ListItem(fOtherwise(Id, Fun, Op)) => .List) _) | |
| rule <stack> | |
| (#incrementInstances(Acc, | |
| (ListItem(fPruning(Id))) XS) | |
| => stack(#reverseList(.List, Acc) ListItem(fPruning(Id)) XS)) | |
| </stack> | |
| <instances>... Id |-> (I => I +Int 1) ...</instances> | |
| rule #incrementInstances((.List => ListItem(fSequential(Param, Fun, Op))) _, | |
| (ListItem(fSequential(Param, Fun, Op)) => .List) _) | |
| rule #incrementInstances((.List => ListItem(fCall(Env))) _, | |
| (ListItem(fCall(Env)) => .List) _) | |
| rule #incrementInstances((.List => ListItem($fResult)) _, | |
| (ListItem($fResult) => .List) _) | |
| syntax PendValue ::= "pendStopped" | |
| | "pend" | |
| syntax Frame ::= fPruning(Int) | |
| | fOtherwise(Int, Int, Int) | |
| | fSequential(Int, Int, Int) | |
| | fCall(Map) | |
| | "$fResult" | |
| syntax RealVal ::= Int | closure(Int, Int, Map) | |
| syntax Val ::= pending(Int) | val(RealVal) | |
| syntax OrcToken ::= OrcToken(Int, Int, Map, Stack) | |
| syntax KResult ::= Val | |
| syntax Stage ::= "INIT" | "RUNNING" | "STOPPED" | |
| configuration <T> | |
| <stage>INIT</stage> | |
| <threads> | |
| <thread multiplicity="*"> | |
| <currentFun>0</currentFun> | |
| <pc>-1</pc> | |
| <k>.:Op</k> | |
| <result>.:Val</result> | |
| <stack>stack(.List)</stack> | |
| <env>.Map</env> | |
| <waitEnv>.Map</waitEnv> | |
| <waitEnvKey>0</waitEnvKey> | |
| </thread> | |
| </threads> | |
| <queue>.List</queue> | |
| <values>.List</values> | |
| <instance> | |
| <currentCoeffect>0</currentCoeffect> | |
| <blocks>.List</blocks> | |
| </instance> | |
| <instances>.Map</instances> | |
| <firstValues>.Map</firstValues> | |
| <pendingValues>.Map</pendingValues> | |
| <ops> | |
| <op multiplicity="*"> | |
| <opFunId>0</opFunId> | |
| <opId>0</opId> | |
| <body>#stop</body> | |
| </op> | |
| </ops> | |
| <initOps>.Map</initOps> | |
| <ffi>.Map</ffi> | |
| <source>$PGM:Source</source> | |
| </T> | |
| rule <source>ffi { _ } Id _ { (OpId : Body) XS => XS } _</source> | |
| <ops> | |
| ... (.Bag => | |
| <op> | |
| <opFunId>Id</opFunId> | |
| <opId>OpId</opId> | |
| <body>Body</body> | |
| </op>) | |
| ...</ops> | |
| rule <source>ffi { _ } (Id (InitId => -1) { _ }) _</source> | |
| <initOps>... .Map => Id |-> InitId ...</initOps> | |
| requires InitId =/=Int -1 | |
| rule <source>ffi { Id Def:String XS => XS } _</source> | |
| <ffi>... .Map => Id |-> Def ...</ffi> | |
| rule <source>ffi { _ } (_ -1 { .SourceOps } XS:SourceFuns => XS)</source> | |
| rule <source>ffi { .SourceFFIs } .SourceFuns => .:Source</source> | |
| // Main thread | |
| rule <threads> | |
| .Bag => <thread> | |
| <currentFun>0</currentFun> | |
| <pc>-1</pc> | |
| <k>.:Op</k> | |
| <result>.:Val</result> | |
| <stack>stack(ListItem($fResult))</stack> | |
| <env>.Map</env> | |
| <waitEnv>.Map</waitEnv> | |
| <waitEnvKey>0</waitEnvKey> | |
| </thread> | |
| </threads> | |
| <stage>INIT => RUNNING</stage> | |
| rule <threads>.Bag</threads> | |
| <stage>RUNNING => STOPPED</stage> | |
| // Init op | |
| rule <thread>... | |
| <currentFun>FunId:Int</currentFun> | |
| <pc>-1 => OpId</pc> | |
| ...</thread> | |
| <initOps>... FunId |-> OpId ...</initOps> | |
| // Place actual op | |
| rule <thread>... | |
| <pc>OpId</pc> | |
| <currentFun>FunId</currentFun> | |
| <k>. => Body</k> | |
| ...</thread> | |
| <op>... | |
| <opFunId>FunId</opFunId> | |
| <opId>OpId</opId> | |
| <body>Body</body> | |
| ...</op> | |
| // Tick | |
| // const | |
| rule <thread>... | |
| <k>#constInt I</k> | |
| <result>.:Val => val(I)</result> | |
| ...</thread> | |
| // parallel | |
| rule <threads>... | |
| <thread>... | |
| <currentFun>Fun</currentFun> | |
| <pc>_ => Op1</pc> | |
| <k>#parallel Op1 Op2 => .</k> | |
| <stack> stack(Stack) => #incrementInstances(.List, Stack)</stack> | |
| <env>Env</env> | |
| ...</thread> | |
| (.Bag => <thread> | |
| <currentFun>Fun</currentFun> | |
| <pc>Op2</pc> | |
| <k>.:Op</k> | |
| <result>.:Val</result> | |
| <stack>stack(Stack)</stack> | |
| <env>Env</env> | |
| <waitEnv>.Map</waitEnv> | |
| <waitEnvKey>0</waitEnvKey> | |
| </thread>) | |
| ...</threads> | |
| // pruning | |
| rule <threads>... | |
| <thread>... | |
| <currentFun>Fun</currentFun> | |
| <pc>_ => Op1</pc> | |
| <k>#pruning Op1 Param Op2 => .</k> | |
| <stack> stack(Stack) => #incrementInstances(.List, Stack)</stack> | |
| <env>Env => Env[Param <- pending(!Id)]</env> | |
| ...</thread> | |
| (.Bag => <thread> | |
| <currentFun>Fun</currentFun> | |
| <pc>Op2</pc> | |
| <k>.:Op</k> | |
| <result>.:Val</result> | |
| <stack>stack(ListItem(fPruning(!Id)) Stack)</stack> | |
| <env>Env</env> | |
| </thread>) | |
| ...</threads> | |
| <instances>... .Map => !Id |-> 1 ...</instances> | |
| <pendingValues>... .Map => !Id |-> pend ...</pendingValues> | |
| requires Param =/=Int -1 | |
| // Otherwise | |
| rule <thread>... | |
| <currentFun>Fun</currentFun> | |
| <pc>_ => Op1</pc> | |
| <k>#otherwise Op1 Op2 => .</k> | |
| <stack>stack(Stack => ListItem(fOtherwise(!Id, Fun, Op2)) Stack)</stack> | |
| ...</thread> | |
| <instances>... .Map => !Id |-> 1 ...</instances> | |
| <firstValues>... .Map => !Id |-> false ...</firstValues> | |
| // Call | |
| rule <thread>... | |
| <k>#callFun Fun [ Param, Params => Params ]</k> | |
| <env>... Param |-> val(Val) ...</env> | |
| <waitEnv>... .Map => WaitEnvKey |-> val(Val)</waitEnv> | |
| <waitEnvKey>WaitEnvKey => WaitEnvKey +Int 1</waitEnvKey> | |
| ...</thread> | |
| rule <thread>... | |
| <k>#callFun Fun [ Param, Params => Params ]</k> | |
| <env>... Param |-> pending(Id) ...</env> | |
| <waitEnv>... .Map => WaitEnvKey |-> val(Val)</waitEnv> | |
| <waitEnvKey>WaitEnvKey => WaitEnvKey +Int 1</waitEnvKey> | |
| ...</thread> | |
| <pendingValues>... Id |-> val(Val) ...</pendingValues> | |
| rule <thread>... | |
| <currentFun>_ => Fun</currentFun> | |
| <pc> _ => -1</pc> | |
| <k>#callFun Fun [ .Ints ] => .:Op</k> | |
| <env>Env => NewEnv</env> | |
| <waitEnv>NewEnv => .Map</waitEnv> | |
| <waitEnvKey>_ => 0</waitEnvKey> | |
| <stack>stack(Stack) => stack(ListItem(fCall(Env)) Stack)</stack> | |
| ...</thread> | |
| // FFI | |
| rule <thread>... | |
| <k>#ffi _ [ Param, Params => Params ]</k> | |
| <env>... Param |-> val(Val) ...</env> | |
| <waitEnv>... .Map => WaitEnvKey |-> val(Val)</waitEnv> | |
| <waitEnvKey>WaitEnvKey => WaitEnvKey +Int 1</waitEnvKey> | |
| ...</thread> | |
| rule <thread>... | |
| <k>#ffi _ [ Param, Params => Params ]</k> | |
| <env>... Param |-> pending(Id) ...</env> | |
| <waitEnv>... .Map => WaitEnvKey |-> val(Val)</waitEnv> | |
| <waitEnvKey>WaitEnvKey => WaitEnvKey +Int 1</waitEnvKey> | |
| ...</thread> | |
| <pendingValues>... Id |-> val(Val) ...</pendingValues> | |
| // Publish | |
| rule <thread>... | |
| <result>val(V)</result> | |
| <stack>stack(ListItem($fResult) XS => XS)</stack> | |
| ...</thread> | |
| <values>.List => ListItem(V) ...</values> | |
| requires V =/=K .:Val | |
| rule <thread>... | |
| <result>V</result> | |
| <stack>stack(ListItem(fPruning(Id)) XS => .List)</stack> | |
| ...</thread> | |
| <pendingValues>... Id |-> (pend => V) ...</pendingValues> | |
| <instances>... Id |-> (I => I -Int 1) ...</instances> | |
| requires V =/=K .:Val | |
| rule <thread>... | |
| <result>V</result> | |
| <stack>stack(ListItem(fPruning(Id)) XS => .List)</stack> | |
| ...</thread> | |
| <pendingValues>... Id |-> val(_) ...</pendingValues> | |
| <instances>... Id |-> (I => I -Int 1) ...</instances> | |
| requires V =/=K .:Val | |
| rule <thread>... | |
| <result>V</result> | |
| <stack>stack(ListItem(fCall(Env)) XS => XS)</stack> | |
| <env>_ => Env</env> | |
| ...</thread> | |
| requires V =/=K .:Val | |
| rule <threads>... | |
| <thread>... | |
| <stack>stack(.List)</stack> | |
| ...</thread> => .Bag | |
| </threads> | |
| // Stop | |
| rule <thread>... | |
| <k>#stop</k> | |
| <stack>stack(ListItem(fCall(Env)) XS => XS)</stack> | |
| ...</thread> | |
| rule <thread>... | |
| <k>#stop</k> | |
| <stack>stack(ListItem($fResult) XS => XS)</stack> | |
| ...</thread> | |
| rule <thread>... | |
| <k>#stop</k> | |
| <stack>stack(ListItem(fPruning(Id)) XS) => .</stack> | |
| ...</thread> | |
| <pendingValues>... Id |-> (pend => pendStopped) ...</pendingValues> | |
| <instances>... Id |-> 1 ...</instances> | |
| rule <thread>... | |
| <k>#stop</k> | |
| <stack>stack(ListItem(fPruning(Id)) XS) => .</stack> | |
| ...</thread> | |
| <instances>... Id |-> (I => I -Int 1)...</instances> | |
| requires I >Int 1 | |
| // Prims | |
| // "core.let" | |
| rule <thread>... | |
| <k>#ffi Id [ .Ints ]</k> | |
| <result>.:Val => Val</result> | |
| <waitEnv>0 |-> Val</waitEnv> | |
| ...</thread> | |
| <ffi>... Id |-> "core.let" ...</ffi> | |
| // "core.add" | |
| rule <thread>... | |
| <k>#ffi Id [ .Ints ]</k> | |
| <result>.:Val => val(X +Int Y) </result> | |
| <waitEnv>0 |-> val(X:Int) 1 |-> val(Y:Int)</waitEnv> | |
| ...</thread> | |
| <ffi>... Id |-> "core.add" ...</ffi> | |
| endmodule |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment