Skip to content

Instantly share code, notes, and snippets.

@prepor
Created February 13, 2018 14:13
Show Gist options
  • Save prepor/b214eac430f2fa8de54b3550f090b584 to your computer and use it in GitHub Desktop.
Save prepor/b214eac430f2fa8de54b3550f090b584 to your computer and use it in GitHub Desktop.
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