diff --git a/Makefile b/Makefile index 6fdaf2fb..c9008b65 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,5 @@ export SCALA_V := 2.13 -export COMPILER_JAR := target/scala-$(SCALA_V)/pdsl.jar +export COMPILER_JAR := target/scala-$(SCALA_V)/pdl.jar export BSV_LOCKS := $(realpath bscRuntime/locks) export BSV_MEMS := $(realpath bscRuntime/memories) diff --git a/README.md b/README.md index bf100d05..ccc94f82 100644 --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ the only supported platform. In the top-level directory of this repo, simply run `make`. -This will produce an executable jar, `pdsl.jar`, in the `target/scala-2.13/` directory +This will produce an executable jar, `pdl.jar`, in the `target/scala-2.13/` directory and will use BSV to compile the custom hardware module libraries. You can also manually build the compiler by running `sbt compile`. @@ -45,7 +45,7 @@ You can also manually build the compiler by running `sbt compile`. The main class is `pipedsl.Main` and can be run via the sbt command `sbt "run pipedsl.Main "`. Alternatively, the executable jar can be used by -running java with the command `java -jar pdsl.jar `. +running java with the command `java -jar pdl.jar `. We also provide a script `pdl` in the `bin` directory that runs the executable jar with the provided arguments. diff --git a/bin/pdl b/bin/pdl index d368076e..6323fb4a 100755 --- a/bin/pdl +++ b/bin/pdl @@ -3,7 +3,7 @@ set -e #execute the pdl compiler -JARNAME=pdsl.jar +JARNAME=pdl.jar JARPATH=target/scala-2.13/"$JARNAME" SCRIPTPATH=$(cd "$(dirname "$0")" && pwd -P) #pass through all cmds except fist diff --git a/build.sbt b/build.sbt index 07b02a8b..e4b1fcf7 100644 --- a/build.sbt +++ b/build.sbt @@ -1,4 +1,4 @@ -name := "PipeDSL" +name := "PipelineDescriptionLanguage" version := "0.0.1" scalaVersion := "2.13.2" @@ -25,6 +25,6 @@ libraryDependencies ++= Seq( ) //Deployment Options -assemblyJarName in assembly := "pdsl.jar" +assemblyJarName in assembly := "pdl.jar" test in assembly := {} mainClass in assembly := Some("pipedsl.Main") \ No newline at end of file diff --git a/examples/Memories b/examples/Memories deleted file mode 100644 index 267bfde4..00000000 --- a/examples/Memories +++ /dev/null @@ -1,21 +0,0 @@ -Memories are the built-in array type for our DSL, -which correspond to any physical memories such as SRAM OR -black box circuits with a memory interface (e.g. some caches) - -Memory Types are written as such: - -elemType[addrSize] - -where elemType is some non-memory type, -and addrSize is a constant of unsigned integer type //TODO support statically evaluatable expressions -which denotes how many bits are required to address the memory. -A memory with addrSize = a, can store 2^a elements. - -This corresponds to the following information about a memory: - -Memory: { - readOut: elemType - writeInt: elemType - addressType: int -} - diff --git a/examples/paper/histogram/histogram.pdl b/examples/histogram/histogram.pdl similarity index 100% rename from examples/paper/histogram/histogram.pdl rename to examples/histogram/histogram.pdl diff --git a/examples/paper/histogram/histogram_bram.pdl b/examples/histogram/histogram_bram.pdl similarity index 100% rename from examples/paper/histogram/histogram_bram.pdl rename to examples/histogram/histogram_bram.pdl diff --git a/examples/paper/histogram/histogram_short.pdl b/examples/histogram/histogram_short.pdl similarity index 100% rename from examples/paper/histogram/histogram_short.pdl rename to examples/histogram/histogram_short.pdl diff --git a/examples/paper/histogram/memInputs/f b/examples/histogram/memInputs/f similarity index 100% rename from examples/paper/histogram/memInputs/f rename to examples/histogram/memInputs/f diff --git a/examples/paper/histogram/memInputs/f_pessimistic b/examples/histogram/memInputs/f_pessimistic similarity index 100% rename from examples/paper/histogram/memInputs/f_pessimistic rename to examples/histogram/memInputs/f_pessimistic diff --git a/examples/paper/histogram/memInputs/h b/examples/histogram/memInputs/h similarity index 100% rename from examples/paper/histogram/memInputs/h rename to examples/histogram/memInputs/h diff --git a/examples/paper/histogram/memInputs/w b/examples/histogram/memInputs/w similarity index 100% rename from examples/paper/histogram/memInputs/w rename to examples/histogram/memInputs/w diff --git a/examples/paper/histogram/testResults/expected b/examples/histogram/testResults/expected similarity index 100% rename from examples/paper/histogram/testResults/expected rename to examples/histogram/testResults/expected diff --git a/examples/paper/histogram/testResults/expected_pessimistic b/examples/histogram/testResults/expected_pessimistic similarity index 100% rename from examples/paper/histogram/testResults/expected_pessimistic rename to examples/histogram/testResults/expected_pessimistic diff --git a/examples/paper/histogram/testResults/results b/examples/histogram/testResults/results similarity index 100% rename from examples/paper/histogram/testResults/results rename to examples/histogram/testResults/results diff --git a/examples/paper/histogram/testResults/results_bram b/examples/histogram/testResults/results_bram similarity index 100% rename from examples/paper/histogram/testResults/results_bram rename to examples/histogram/testResults/results_bram diff --git a/examples/paper/histogram/testResults/results_pessimistic b/examples/histogram/testResults/results_pessimistic similarity index 100% rename from examples/paper/histogram/testResults/results_pessimistic rename to examples/histogram/testResults/results_pessimistic diff --git a/examples/paper/histogram/testResults/results_pessimistic_bram b/examples/histogram/testResults/results_pessimistic_bram similarity index 100% rename from examples/paper/histogram/testResults/results_pessimistic_bram rename to examples/histogram/testResults/results_pessimistic_bram diff --git a/examples/paper/histogram/testResults/results_pessimistic_short b/examples/histogram/testResults/results_pessimistic_short similarity index 100% rename from examples/paper/histogram/testResults/results_pessimistic_short rename to examples/histogram/testResults/results_pessimistic_short diff --git a/examples/paper/histogram/testResults/results_short b/examples/histogram/testResults/results_short similarity index 100% rename from examples/paper/histogram/testResults/results_short rename to examples/histogram/testResults/results_short diff --git a/examples/hls/bfs b/examples/hls/bfs deleted file mode 100644 index 3dbc97f8..00000000 --- a/examples/hls/bfs +++ /dev/null @@ -1,32 +0,0 @@ - -pipe bfs()[nodes[N_NODES], edges[N_EDGES], levels[N_NODES], level_counts[N_LEVELS]] { - node_index_t n; - edge_index_t e; - level_t horizon; - edge_index_t cnt; - - level[starting_node] = 0; - level_counts[0] = 1; - - loop_horizons: for( horizon=0; horizon)[feature: int<32>[7], weight: int<32>[7], h: int<32>[32]] { - if (counter < 127<7>) { - call hist(counter + 1<7>); - } //else no next loop iteration, done - start(feature); - start(weight); - acquire(feature[counter]); - acquire(weight[counter]); - int<32> m = feature[counter]; - int<32> wt = weight[counter]; - release(feature[counter]); - release(weight[counter]); - end(feature); - end(weight); - --- - start(h); - acquire(h[m]); - end(h); - - int<32> nm = h[m] + wt; //many ways to break this section up for scheduling - --- - h[m] <- nm; - release(h[m]); -} - -circuit { - f = regfile(int<32>, 7); - w = regfile(int<32>, 7); - h = regfile(int<32>, 32); - hg = new hist[f, w, h]; - call hg(0<7>); -} \ No newline at end of file diff --git a/examples/hls/simpleloop b/examples/hls/simpleloop deleted file mode 100644 index cf467fea..00000000 --- a/examples/hls/simpleloop +++ /dev/null @@ -1,61 +0,0 @@ -/* -s = 0; -for(int i = 0; i < 100; i++) { - d = A[i] - B[i]; - if (d > 0) { - s += d; - } -} -return s; -*/ - -pipe sum(counter: int<7>)[memA: int<30>[7], memB: int<30>[7], total: int<30>[1]] { - if (counter < 100<7>) { - call sum(counter + 1<7>); - //acquire(memA[counter]); - start(memA); - acquire(memA); - end(memA); - start(memB); - acquire(memB); - end(memB); - int<30> argA <- memA[counter]; - int<30> argB <- memB[counter]; - //release(memA[counter]); - release(memA); - //release(memB[counter]); - release(memB); - --- - int<30> d = 1<30>; //could split into multiple cycles as in HLS examples - if (d > 0<30>) { - --- - start(total); - acquire(total); - end(total); - int<30> s = total[0] + d; //could split into multiple cycles as in HLS - print(s); - total[0] <- s; - release(total); - } - } //else done, do nothing -} - -/* - start(total); - reserve(total[0]); - int<32> t0 = bypass(total[0]); - int<32> s = t0 + d; - end(total); - --- - acquire(total[0]); - total[0] <- s; - release(total); - -*/ -circuit { - total = regfile(int<30>, 1); - memA = memory(int<30>, 7); - memB = memory(int<30>, 7); - s = new sum[memA, memB, total]; - call s(0<7>); -} \ No newline at end of file diff --git a/examples/paper/matpow/matpow.pdl b/examples/matpow/matpow.pdl similarity index 100% rename from examples/paper/matpow/matpow.pdl rename to examples/matpow/matpow.pdl diff --git a/examples/paper/matpow/matpow_alt.pdl b/examples/matpow/matpow_alt.pdl similarity index 100% rename from examples/paper/matpow/matpow_alt.pdl rename to examples/matpow/matpow_alt.pdl diff --git a/examples/paper/matpow/matpow_bram.pdl b/examples/matpow/matpow_bram.pdl similarity index 100% rename from examples/paper/matpow/matpow_bram.pdl rename to examples/matpow/matpow_bram.pdl diff --git a/examples/paper/matpow/memInputs/a_16 b/examples/matpow/memInputs/a_16 similarity index 100% rename from examples/paper/matpow/memInputs/a_16 rename to examples/matpow/memInputs/a_16 diff --git a/examples/paper/matpow/memInputs/a_2 b/examples/matpow/memInputs/a_2 similarity index 100% rename from examples/paper/matpow/memInputs/a_2 rename to examples/matpow/memInputs/a_2 diff --git a/examples/paper/matpow/memInputs/a_4 b/examples/matpow/memInputs/a_4 similarity index 100% rename from examples/paper/matpow/memInputs/a_4 rename to examples/matpow/memInputs/a_4 diff --git a/examples/paper/matpow/memInputs/a_8 b/examples/matpow/memInputs/a_8 similarity index 100% rename from examples/paper/matpow/memInputs/a_8 rename to examples/matpow/memInputs/a_8 diff --git a/examples/paper/matpow/memInputs/c b/examples/matpow/memInputs/c similarity index 100% rename from examples/paper/matpow/memInputs/c rename to examples/matpow/memInputs/c diff --git a/examples/paper/matpow/memInputs/r b/examples/matpow/memInputs/r similarity index 100% rename from examples/paper/matpow/memInputs/r rename to examples/matpow/memInputs/r diff --git a/examples/paper/matpow/memInputs/x b/examples/matpow/memInputs/x similarity index 100% rename from examples/paper/matpow/memInputs/x rename to examples/matpow/memInputs/x diff --git a/examples/paper/matpow/testResults/expected_2 b/examples/matpow/testResults/expected_2 similarity index 100% rename from examples/paper/matpow/testResults/expected_2 rename to examples/matpow/testResults/expected_2 diff --git a/examples/paper/matpow/testResults/expected_4 b/examples/matpow/testResults/expected_4 similarity index 100% rename from examples/paper/matpow/testResults/expected_4 rename to examples/matpow/testResults/expected_4 diff --git a/examples/paper/matpow/testResults/results_2 b/examples/matpow/testResults/results_2 similarity index 100% rename from examples/paper/matpow/testResults/results_2 rename to examples/matpow/testResults/results_2 diff --git a/examples/paper/matpow/testResults/results_2_alt b/examples/matpow/testResults/results_2_alt similarity index 100% rename from examples/paper/matpow/testResults/results_2_alt rename to examples/matpow/testResults/results_2_alt diff --git a/examples/paper/matpow/testResults/results_2_bram b/examples/matpow/testResults/results_2_bram similarity index 100% rename from examples/paper/matpow/testResults/results_2_bram rename to examples/matpow/testResults/results_2_bram diff --git a/examples/paper/matpow/testResults/results_4 b/examples/matpow/testResults/results_4 similarity index 100% rename from examples/paper/matpow/testResults/results_4 rename to examples/matpow/testResults/results_4 diff --git a/examples/paper/matpow/testResults/results_4_alt b/examples/matpow/testResults/results_4_alt similarity index 100% rename from examples/paper/matpow/testResults/results_4_alt rename to examples/matpow/testResults/results_4_alt diff --git a/examples/paper/matpow/testResults/results_4_bram b/examples/matpow/testResults/results_4_bram similarity index 100% rename from examples/paper/matpow/testResults/results_4_bram rename to examples/matpow/testResults/results_4_bram diff --git a/examples/modules/functional.pdsl b/examples/modules/functional.pdsl deleted file mode 100644 index c734116a..00000000 --- a/examples/modules/functional.pdsl +++ /dev/null @@ -1,116 +0,0 @@ -/* - * This file has examples of so-called "functional" modules. - * These modules (unlike, for example, memories) have no internal state - * but simply process requests and produce outputs. - * Importantly, they are pipelined, and can process multiple requests at once. - */ - -//note the return type after the ':' -pipe mult(d1: int<32>, d2: int<32>)[]: int<32> { - //do stuff stage 1 - --- - //do stuff stage 2 - --- - //do stuff stage 3 - --- - //output the result on this stage - output(d1 * d2); - //this involves placing it on an output queue - //which the client will read from -} - -//This is an example client that might use the multiplier. - -pipe client(pc: int<32>)[inputs: int<32>[32], outputs: int<32>[1], m: mult] { - start(inputs); - start(outputs); - acquire(inputs); - reserve(outputs); - end(inputs); - end(outputs); - int<32> a1 <- inputs[pc]; - call client(pc + 1<32>); - --- - int<32> a2 <- inputs[pc + 1<32>]; - --- - release(inputs); - if (cast (pc{0:0}, bool)) { - start(m); - acquire(m); - int<32> result <- call m(a1+a1, a2); - release(m); - end(m); - int<1> zzz = 1<1>; - int<1> aaa = 1<1>; - --- - } else { - int<32> result = 10<32>; - } - --- - block(outputs); - outputs[0<1>] <- result; - release(outputs); - --- -} - -//This is a 3-stage pipeline: read inputs -> call mult -> recv mult/ write outputs - -//This has the problem that only 3 instructions can be processed at a time, even though the multiplier is pipelined. -//If we consider that each of those '->' to be queues (which the current code generator does) -//Then we *actually* can fill the pipeline with more instructions. - -//We can imagine a pass where we "balance" these queue sizes based on the depth of -//called modules, but that is an extra, late-stage optimization - - -//Now let's consider a pipeline where this is called in multiple conditional paths -/* -pipe multiclient(pc: int<32>)[inputs: int<32>[32], outputs: int<32>[1], m: mult] { - acquire(inputs); - call multiclient(pc + 2<32>); - if (pc{0:0} == 0<1>) { - int<32> a1 <- inputs[pc]; - release(inputs); - --- - int<32> result <- call mult(a1, a1); - } else { - int<32> a2 <- inputs[pc + 1<32>]; - release(inputs); - --- - int<32> result <- call mult(a2+a2, a2); - } - --- - acquire(outputs); - outputs[pc] <- result; - release(outputs); -} -*/ -//Now we need to reason about ordering of the calls to `mult`. -//In theory both of the stages that `call mult` can be running in parallel. -//There is currently no way to resolve which one should execute first and therefore -//also receive the output first. - -//We could just use locks as before: - -/* - reserve(mult); - if (...); { - --- - acquire(mult); - int<32> result <- mult(..); - } else { - --- - acquire(mult); - int<32> result <- mult(..); - } - release(mult); -*/ - - -circuit { - m = new mult[]; - ins = memory(int<32>, 32); - outs = memory(int<32>, 1); - p = new client[ins, outs, m]; - call p(0<32>); -} diff --git a/examples/modules/lockregion.pdsl b/examples/modules/lockregion.pdsl deleted file mode 100644 index 2d3af7f7..00000000 --- a/examples/modules/lockregion.pdsl +++ /dev/null @@ -1,14 +0,0 @@ -pipe client(pc: int<32>)[inputs: int<32>[32]] { - start(inputs); - acquire(inputs); - int<32> x <- inputs[pc]; - --- - end(inputs); - release(inputs); -} - -circuit { - ins = memory(int<32>, 32); - p = new client[ins]; - call p(0<32>); -} \ No newline at end of file diff --git a/examples/paper/multiExec/imemMultiExec b/examples/multiExec/imemMultiExec similarity index 100% rename from examples/paper/multiExec/imemMultiExec rename to examples/multiExec/imemMultiExec diff --git a/examples/paper/multiExec/multiexec.pdl b/examples/multiExec/multiexec.pdl similarity index 100% rename from examples/paper/multiExec/multiexec.pdl rename to examples/multiExec/multiexec.pdl diff --git a/examples/paper/multiExec/multiexec_alt.pdl b/examples/multiExec/multiexec_alt.pdl similarity index 100% rename from examples/paper/multiExec/multiexec_alt.pdl rename to examples/multiExec/multiexec_alt.pdl diff --git a/examples/paper/multiExec/multiexec_split.pdl b/examples/multiExec/multiexec_split.pdl similarity index 100% rename from examples/paper/multiExec/multiexec_split.pdl rename to examples/multiExec/multiexec_split.pdl diff --git a/examples/paper/multiExec/rfMultiExec b/examples/multiExec/rfMultiExec similarity index 100% rename from examples/paper/multiExec/rfMultiExec rename to examples/multiExec/rfMultiExec diff --git a/examples/pipeDSL/addr-lock-tests.pdsl b/examples/pipeDSL/addr-lock-tests.pdsl deleted file mode 100644 index fda2eb8b..00000000 --- a/examples/pipeDSL/addr-lock-tests.pdsl +++ /dev/null @@ -1,120 +0,0 @@ -pipe ex1(in: bool)[r1: int<32>[5], r2: int<32>[5]] { - start(r1); - start(r2); - int<5> addr = 1<5>; - if (in) { - reserve(r1[addr]); - } else { - reserve(r2[addr]); - } - end(r1); - end(r2); - --- - if (in) { - block(r1[addr]); - r1[addr] <- 32<32>; - release(r1[addr]); - } - --- - if (!in) { - block(r2[addr]); - r2[addr] <- 32<32>; - release(r2[addr]); - } -} - -pipe ex2(in: bool)[rf: int<32>[5]] { - start(rf); - int<5> addr = 1<5>; - if (in) { - reserve(rf[addr]); - } - //maybe reserved = { addr, addr_handle } - --- - int<5> addr2 = 2<5>; - bool cond2 = true; - if (cond2) { - reserve(rf[addr2]); - //if(addr_handle_valid && addr == addr2) addr2_handle = addr_handle - } - //maybe reserved = { addr, addr_handle; addr2, addr2_handle } - --- - if (in) { - block(rf[addr]); //no change - release(rf[addr]); - //if(addr2_handle_valid && addr == addr2) { addr_1_handle = invalid } else { release(addr_handle) }; - } - //maybe reserved = { addr, addr_handle; addr2, addr2_handle } - end(rf); - --- - if (cond2) { - block(rf[addr2]); //no change - release(rf[addr2]); - //if(addr_handle_valid && addr == addr2) { No-Op } else {release(addr2_handle) }; - } -} - -pipe ex3(in: bool)[rf: int<32>[5]] { - start(rf); - int<5> addr1 = 0<5>; - int<5> addr2 = 1<5>; - int<5> addr3 = 2<5>; - acquire(rf[addr1]); //checkfree - acquire(rf[addr2]); //checkfree && reserve - reserve(rf[addr3]); //reserve - release(rf[addr1]); - end(rf); - //becomes: - //checkfree(addr1) && checkfree(addr2) - //reserve(addr2) - //if (addr2 == addr3) addr3_handle = addr2_handle else reserve(addr3) - //maybe reserved = { addr2, addr2_handle; addr3, addr3_handle } - --- - release(rf[addr2]); - //if (addr2 == addr3 && addr3_handle_valid) { addr2_handle = invalid } else { release(addr2_handle) }; - block(rf[addr3]); - --- - release(rf[addr3]); -} - -pipe ex4(input: int<32>)[rf: int<32>[5]] { - - start(rf); - int<5> a1 = 0<5>; - int<5> a2 = 1<5>; - bool b1 = cast(input{0:0} == 1, bool); - bool b2 = cast(input{1:1} == 1, bool); - reserve(rf[a2]); - if (b1) { - reserve(rf[a1]); - } else { - reserve(rf[a1]); - } - end(rf); - if (b1) { - block(rf[a1]); - if (b2) { - release(rf[a1]); - } - } - --- - if(b1) { - block(rf[a2]); - release(rf[a2]); - } else { - block(rf[a2]); - release(rf[a2]); - } - if (b1 && (!b2)) { - release(rf[a1]); - } else { - if(!b1) { - block(rf[a1]); - release(rf[a1]); - } - } -} - -circuit { - r = memory(int<32>, 5); -} \ No newline at end of file diff --git a/examples/pipeDSL/branch-tests.pdsl b/examples/pipeDSL/branch-tests.pdsl deleted file mode 100644 index 497721b9..00000000 --- a/examples/pipeDSL/branch-tests.pdsl +++ /dev/null @@ -1,71 +0,0 @@ -pipe test1(input: int<32>)[rf: int<32>[5]] { - if (input == 0) { - call test1(input + 1<32>); - } - start(rf); - acquire(rf); - end(rf); - if (input{0:0} == 1) { - rf[input{4:0}] <- input; - --- - int<32> y = input; - --- - int<32> z = input; - } else { - int<32> x = input; - } - release(rf); - --- -} - -pipe test2(input: int<32>)[rf: int<32>[5]] { - start(rf); - acquire(rf); - end(rf); - if (input{0:0} == 1) { - int<32> y = 4<32>; - } else { - int<32> y <- rf[input{4:0}]; - --- - } - release(rf); - call test2(y); -} - -pipe test3(input: int<32>)[] { - if (input{0:0} == 1) { - if (input{1:1} == 0) { - int<2> x = 0<2>; - int<2> y = 1<2>; - } else { - int<2> x = 1<2>; - } - } else { - if (input{2:2} == 0) { - int<2> x = 3<2>; - } else { - int<2> x = 4<2>; - } - } - call test3(0<30> ++ x); -} - -pipe test4(input: int<32>)[] { - if (cast (input{0:0}, bool)) { - if (input{1:1} == 0) { - int<2> x = 0<2>; - } else { - --- - int<2> x = 1<2>; - } - } else { - int<2> x = 3<2>; - } - call test4(0<30> ++ x); -} - -circuit { - r = memory(int<32>, 5); - t = new test1[r]; - call t(0<32>); -} \ No newline at end of file diff --git a/examples/pipeDSL/interpreter-simple-test.pdsl b/examples/pipeDSL/interpreter-simple-test.pdsl deleted file mode 100644 index 3fa6dd15..00000000 --- a/examples/pipeDSL/interpreter-simple-test.pdsl +++ /dev/null @@ -1,11 +0,0 @@ -pipe cpu(pc:int<32>)[rf: int<32>[5]] { - acquire(rf); - rf[0<5>] <- rf[0<5>] + 1<32>; - release(rf); - call cpu(0<32>); -} - -circuit { - r = memory(int<32>, 5); - c = new cpu(0<32>)[r]; -} \ No newline at end of file diff --git a/examples/pipeDSL/lock-tests.pdsl b/examples/pipeDSL/lock-tests.pdsl deleted file mode 100644 index f5a44e29..00000000 --- a/examples/pipeDSL/lock-tests.pdsl +++ /dev/null @@ -1,275 +0,0 @@ -/*Expected Fail since acquired inside branch and not released -pipe test1(input: int<32>)[rf: int<32>[5]] { - if (input{0:0} == 1) { - reserve(rf); - acquire(rf); - } - release(rf); -} */ -// Expected Success -pipe test2(input: int<32>)[rf: int<32>[5]] { - if (input{0:0} == 1) { - start(rf); - acquire(rf); - release(rf); - end(rf); - } -} -/* Expected failure since not released in both branches -pipe test3(input: int<32>)[rf: int<32>[5]] { - reserve(rf); - acquire(rf); - if (input{0:0} == 1) { - int<32> arg <- rf[input{4:0}]; - release(rf); - } -} */ -/* Expected failure since acquired in both branches -pipe test4(input: int<32>)[rf: int<32>[5]] { - - if (input{0:0} == 1) { - reserve(rf); - acquire(rf); - int<32> arg <- rf[input{4:0}]; - release(rf); - } else { - --- - reserve(rf); - acquire(rf); - --- - release(rf); - } -} */ -//Expected Success -pipe test5(input: int<32>)[rf: int<32>[5]] { - start(rf); - acquire(rf); - end(rf); - --- - if (input{0:0} == 1) { - release(rf); - } else { - int<32> arg <- rf[input{31:27}]; - release(rf); - --- - } -} -/* Expected Failure, must acquire before mem op -pipe test6(input: int<32>)[rf: int<32>[5]] { - reserve(rf); - if (input{0:0} == 1) { - int<32> arg <- rf[input{31:27}]; - release(rf); - } else { - int<32> arg <- rf[input{31:27}]; - release(rf); - } -} */ -/* Expected fail, must acquire first -pipe test7(input: int<32>)[rf: int<32>[5]] { - reserve(rf); - if (input{0:0} == 1) { - release(rf); - } else { - release(rf); - } -} */ -//Expected success since reserve is before branch -pipe test8(input: int<32>)[rf: int<32>[5]] { - start(rf); - reserve(rf); - end(rf); - if (input{0:0} == 1) { - --- - block(rf); - int<32> out <- rf[0<5>]; - } else { - --- - block(rf); - int<32> out <- rf[1<5>]; - } - --- - rf[2<5>] <- out; - release(rf); - --- -} -//Expected success -pipe test9(input: int<32>)[rf: int<32>[5], dmem: int<32>[32]] { - start(dmem); - reserve(dmem); - end(dmem); - if (input{0:0} == 1) { - start(rf); - acquire(rf); - release(rf); - end(rf); - } - block(dmem); - release(dmem); -} -//Expected success -/* -pipe test10(input: int<32>)[rf: int<32>[5], dmem: int<32>[32]] { - speculate(int<1> x = 1, { - x = 1; - }, { - acquire(rf); - }) - --- - release(rf); -} */ -/* Expected failure since speculation may happen before acquire -pipe test11(input: int<32>)[rf: int<32>[5], dmem: int<32>[32]] { - speculate(int<1> x = 1, { - acquire(rf); - x = 1; - }, { - int<32> y <- rf[x ++ 0<4>]; - }) - --- - release(rf); -} */ -// Expect success -/* -pipe test12(input: int<32>)[rf: int<32>[5], dmem: int<32>[32]] { - acquire(rf); - speculate(int<1> x = 1, { - x = 1; - }, { - int<32> y <- rf[x ++ 0<4>]; - }) - --- - release(rf); -}*/ -/* Expected failure since speculation may happen after release -pipe test13(input: int<32>)[rf: int<32>[5], dmem: int<32>[32]] { - acquire(rf); - speculate(int<1> x = 1, { - release(rf); - x = 1; - }, { - int<32> y <- rf[x ++ 0<4>]; - }) -} */ -/* Expected failure since release operations aren't allowed in speculation -pipe test14(input: int<32>)[rf: int<32>[5], dmem: int<32>[32]] { - acquire(rf); - speculate(int<1> x = 1, { - x = 1; - }, { - release(rf); - }) -} */ - -//Expected Success -pipe test15(input: int<32>)[rf: int<32>[5]] { - bool a = true; - start(rf); - if (a) { - reserve(rf); - } - end(rf); - if (a) { - block(rf); - } - if (a) { - release(rf); - } -} - -/*Expected Failure -pipe test16(input: int<32>)[rf: int<32>[5]] { - int<32> y = 3<32>; - int<32> x = 0<32>; - start(rf); - if (x == y + 3<32>) { - reserve(rf); - } - if (x == 10<32>) { - reserve(rf); - } - end(rf); -} -*/ - -//Expected Success -pipe test17(input: int<32>, randomBool: bool, randomBool2: bool)[rf: int<32>[5]] { - bool a = true; - bool b = false; - if (randomBool == a) { - if (randomBool2 == b){ - start(rf); - reserve(rf); - end(rf); - } - } - if (randomBool == a) { - if (randomBool2 == b){ - block(rf); - } - } - if (randomBool == a) { - if (randomBool2 == b){ - release(rf); - } - } -} - -pipe test18(input: int<32>)[rf: int<32>[5]] { - start(rf); - if (input{0:0} == 1) { - reserve(rf); - } else { - reserve(rf); - } - end(rf); - block(rf); - release(rf); -} - -pipe test19(input: int<32>)[rf: int<32>[5]] { - - start(rf); - bool b1 = cast(input{0:0} == 1, bool); - bool b2 = cast(input{1:1} == 1, bool); - if (b1) { - reserve(rf); - } else { - reserve(rf); - } - end(rf); - if (b1) { - block(rf); - if (b2) { - release(rf); - } - } - --- - if (b1 && (!b2)) { - release(rf); - } else { - if(!b1) { - block(rf); - release(rf); - } - } -} - -pipe test20(input: int<32>)[rf: int<32>[5]] { - start(rf); - int<5> addr1 = input{4:0}; - int<5> addr2 = input{9:5}; - acquire(rf[addr1]); - --- - //{ rf: addr1} - acquire(rf[addr2]); // if ( addr1 == addr2 ) lid_2 = lid_1 else { lid_2 = acquire(addr2) } - end(rf); - --- - release(rf[addr2]); - --- - release(rf[addr1]); -} - -circuit { - r = memory(int<32>, 5); -} \ No newline at end of file diff --git a/examples/pipeDSL/readwritelockex.pdl b/examples/pipeDSL/readwritelockex.pdl deleted file mode 100644 index 62988f8c..00000000 --- a/examples/pipeDSL/readwritelockex.pdl +++ /dev/null @@ -1,73 +0,0 @@ -pipe cpu(pc: int<16>)[rf: int<32>[5], imem: int<32>[16]] { - if (pc < 14<16>) { - call cpu(pc + 1<16>); - } - start(imem); - acquire(imem); - int<32> insn <- imem[pc]; - release(imem); - end(imem); - --- - int<2> op = insn{1:0}; - int<5> rs1 = insn{6:2}; - int<5> rs2 = insn{11:7}; - int<5> rd = insn{16:12}; - start(rf); - acquire(rf[rs1], r); //turns into just a check that no outstanding writes - int<32> rf1 = rf[rs1]; - release(rf[rs1]); - reserve(rf[rs2], r); //reserve read lock (prevents acquisition of write lock? or does nothing ?) - reserve(rf[rd], w); //reserve write lock - /* - reserve(addr, w) => returns new physical address (unused index from circular buffer) - blocks if circular buffer is full - updates "read map" (i.e. which physical address read requests go to) - reserve(addr, r) => returns correct physical address - - block(addr, w) => is this necessary? - block(addr, r) => checks to see if they physical entry (obtained from reserve) had valid data yet - - release(addr, w) => allows new thread to re-use the physical address? - release(addr, r) => not...sure - */ - end(rf); - --- - block(rf[rs2]); - int<32> rf2 = rf[rs2]; - release(rf[rs2]); - --- - int<32> res = rf1 + rf2; - --- - block(rf[rd]); - print(res); - rf[rd] <- res; - release(rf[rd]); - --- -} - -/* - reserve(rf[rs1], r); //create entry in queue - reserve(rf[rs2]); //create entry in queue - reserve(rf[rd]); //create entry in queue - --- - block(rf[rs1]); //wait until entry is head of queue - x = bypass(rf[rs1]); //OR until prior entry has valid data - release(rf[rs1]); //what do if not at head of queue? - --- - block(rf[rs1]); //same as prior - y = rf[rs2]; - release(rf[rs2]); - --- - o = x + y; - commit(rf[rd], o); //write data to queue - --- - block(rf[rd]); //wait until at head of queue - rf[rd] <- o; - release(rf[rd]); //free queue entry -*/ -circuit { - i = memory(int<32>, 16); - r = regfile(int<32>, 5); - c = new cpu[r, i]; - call c(0<16>); -} \ No newline at end of file diff --git a/examples/pipeDSL/simple-interpreter-pipe-test.pdsl b/examples/pipeDSL/simple-interpreter-pipe-test.pdsl deleted file mode 100644 index 58294f7f..00000000 --- a/examples/pipeDSL/simple-interpreter-pipe-test.pdsl +++ /dev/null @@ -1,42 +0,0 @@ -def alu(arg1: int<32>, arg2: int<32>, op: int<2>): int<32> { - if (op == 1<2>) { - return arg1 + arg2; - } else if (op == 2<2>) { - return arg1 >> arg2; - } else if (op == 3<2>) { - return arg1 - arg2; - } else { - return arg1 * arg2; - } -} -pipe cpu(pc: int<5>)[rf: int<32>[5], imem: int<32>[5], dmem: int<32>[5]] { - acquire(imem); - int<32> insn <- imem[pc]; - release(imem); - --- - int<2> op_type = insn{1:0}; - int<2> op = insn{3:2}; - int<5> rs1 = insn{8:4}; - int<5> rs2 = insn{13:9}; - int<5> rd = insn{18:14}; - int<13> imm = insn{31:19}; - acquire(rf); - int<32> arg1 <- rf[rs1]; - int<32> arg2 <- rf[rs2]; - --- - //op_type == ALU; - int<32> add_arg2 = (op_type == 0b1<2>) ? arg2 : 0x0<19> ++ imm; - int<32> alu_res = alu(arg1, add_arg2, op); - --- - rf[rd] <- alu_res; - release(rf); - call cpu(pc + 1<5>); -} - -circuit { - i = memory(int<32>, 5); - d = memory(int<32>, 5); - r = memory(int<32>, 5); - c = new cpu[r, i, d]; - call c(0<5>); -} \ No newline at end of file diff --git a/examples/pipeDSL/simple-pipe-location-specific-locks.pdsl b/examples/pipeDSL/simple-pipe-location-specific-locks.pdsl deleted file mode 100644 index 28e487fe..00000000 --- a/examples/pipeDSL/simple-pipe-location-specific-locks.pdsl +++ /dev/null @@ -1,50 +0,0 @@ -def alu(arg1: int<32>, arg2: int<32>, op: int<2>): int<32> { - if (op == 1<2>) { - return arg1 + arg2; - } else if (op == 2<2>) { - return arg1 >> arg2; - } else if (op == 3<2>) { - return arg1 - arg2; - } else { - return arg1 * arg2; - } -} -pipe cpu(pc: int<32>)[rf: int<32>[5], imem: int<32>[32], dmem: int<32>[32]] { - acquire(imem[pc]); - int<32> insn <- imem[pc]; - release(imem[pc]); - --- - int<2> op_type = insn{1:0}; - int<2> op = insn{3:2}; - int<5> rs1 = insn{8:4}; - int<5> rs2 = insn{13:9}; - int<5> rd = insn{18:14}; - int<13> imm = insn{31:19}; - acquire(rf[rs1]); - acquire(rf[rs2]); - int<32> arg1 = rf[rs1]; - int<32> arg2 = rf[rs2]; - --- - //do some long operation here that doesn't use arg1 or arg2 - int<7> x = imm{6:0}; - //hello - --- - //op_type == BR; - int<32> offset = ((op_type == 0b0<2>) && (arg1 == arg2)) ? 0b0<19> ++ imm : 4<32>; - int<32> npc = pc + offset; - //op_type == ALU; - int<32> add_arg2 = (op_type == 0b1<2>) ? arg2 : 0x0<19> ++ imm; - int<32> alu_res = alu(arg1, add_arg2, op); - --- - rf[rd] <- alu_res; - release(rf[rs1]); - release(rf[rs2]); - call cpu(npc); -} - -circuit { - i = memory(int<32>, 32); - d = memory(int<32>, 32); - r = regfile(int<32>, 5); - c = new cpu(0<32>)[r, i, d]; -} \ No newline at end of file diff --git a/examples/pipeDSL/simple-pipe.pdsl b/examples/pipeDSL/simple-pipe.pdsl deleted file mode 100644 index 636f3bbc..00000000 --- a/examples/pipeDSL/simple-pipe.pdsl +++ /dev/null @@ -1,64 +0,0 @@ -def alu(arg1: int<32>, arg2: int<32>, op: int<2>): int<32> { - if (op == 1<2>) { - return arg1 + arg2; - } else if (op == 2<2>) { - return arg1 >> arg2; - } else if (op == 3<2>) { - return arg1 - arg2; - } else { - return arg1 * arg2; - } -} -pipe cpu(pc: int<32>)[rf: int<32>[5], imem: int<32>[32], dmem: int<32>[32]] { - start(imem); - acquire(imem); - end(imem); - int<32> insn <- imem[pc]; - release(imem); - --- - int<2> op_type = insn{1:0}; - int<2> op = insn{3:2}; - int<5> rs1 = insn{8:4}; - int<5> rs2 = insn{13:9}; - int<5> rd = insn{18:14}; - int<13> imm = insn{31:19}; - start(rf); - acquire(rf[rs1]); - acquire(rf[rs2]); - reserve(rf[rd]); - end(rf); - int<32> arg1 = rf[rs1]; - int<32> arg2 = rf[rs2]; - release(rf[rs1]); - release(rf[rs2]); - --- - //do some long operation here that doesn't use arg1 or arg2 - if (imm{0:0} == 1<1>) { - int<7> x = imm{6:0}; - } else { - int<7> x = imm{12:6}; - } - - //hello - --- - //op_type == BR; - int<32> offset = ((op_type == 0b0<2>) && (arg1 == arg2)) ? 0b0<19> ++ imm : 4<32>; - int<32> npc = pc + offset; - //op_type == ALU; - int<32> add_arg2 = (op_type == 0b1<2>) ? arg2 : 0x0<19> ++ imm; - int<32> alu_res = alu(arg1, add_arg2, op); - --- - block(rf[rd]); - rf[rd] <- alu_res; - release(rf[rd]); - call cpu(npc); - --- -} - -circuit { - i = memory(int<32>, 32); - d = memory(int<32>, 32); - r = regfile(int<32>, 5); - c = new cpu[r, i, d]; - call c(0<32>); -} \ No newline at end of file diff --git a/examples/pipeDSL/small-pipe.pdsl b/examples/pipeDSL/small-pipe.pdsl deleted file mode 100644 index 45a4ae4c..00000000 --- a/examples/pipeDSL/small-pipe.pdsl +++ /dev/null @@ -1,35 +0,0 @@ -pipe cpu(pc: int<32>)[rf: int<32>[5], imem: int<16>[32]] { - start(imem); - acquire(imem); - end(imem); - int<16> insn <- imem[pc]; - release(imem); - --- - int<1> op_type = insn{0:0}; - int<5> rs1 = insn{5:1}; - int<5> rs2 = insn{10:6}; - int<5> rd = insn{15:11}; - start(rf); - acquire(rf); - int<32> arg1 = rf[rs1]; - int<32> arg2 = rf[rs2]; - end(rf); - --- - int<32> offset = ((op_type == 0b0<1>) && (arg1 == arg2)) ? 0b0<27> ++ rd : 4<32>; - int<32> npc = pc + offset; - int<32> alu_res = arg1 + arg2; - call cpu(npc); - --- - int<32> tmp = 0b1<32>; - if (op_type == 0b1<1>) { - rf[rd] <- alu_res + tmp; - } - release(rf); -} - -circuit { - i = memory(int<16>, 32); - r = regfile(int<32>, 5); - c = new cpu[r, i]; - call c(0<32>); -} \ No newline at end of file diff --git a/examples/paper/risc-pipe/risc-pipe-branches.pdl b/examples/risc-pipe/risc-pipe-branches.pdl similarity index 100% rename from examples/paper/risc-pipe/risc-pipe-branches.pdl rename to examples/risc-pipe/risc-pipe-branches.pdl diff --git a/examples/paper/risc-pipe/risc-pipe.pdl b/examples/risc-pipe/risc-pipe.pdl similarity index 100% rename from examples/paper/risc-pipe/risc-pipe.pdl rename to examples/risc-pipe/risc-pipe.pdl diff --git a/examples/speculation/npc.pdl b/examples/speculation/npc.pdl deleted file mode 100644 index 5d944dc2..00000000 --- a/examples/speculation/npc.pdl +++ /dev/null @@ -1,48 +0,0 @@ -spec pipe cpu(pc: int<32>)[rf, imem, dmem] { - insn <- imem[pc]; - sid <- spec call cpu(pc + 4); //creates entry indexed by sid, stores pc + 4); - --- - rs1 = insn{4:0}; - //etc - arg1 = rf[rs1]; - --- - npc = brUnit(arg1, arg2, pc, op); - spec_barrier(); //must be sure that I'm not speculative before verifying speculation I caused - /* - shouldKill = checkSpec(_thread_sid_); //"free"s entry in spec table - if (shouldKill) { - kill(); //stop executing this thread - } else { NOP} - */ - - mispredict = verify call cpu(npc, sid); //updates spec entry w/ mispredict bit - /* want this to be implicit - if (mispredict) { - call cpu(npc); - } */ - /* want this to be specifiable by the programmer in _some_ way */ - update_bpred(pc, npc, mispredict); - --- - //mem stage - --- - if (isWB) { - rf[rd] <- result; - } -} - -//in normal pipeline: just _always_ call cpu(pc + 4) in stage 1. -//in stage 3, if npc != pc + 4, then kill stage 1 and stage 2 AND call cpu(pc + 4) - - -//what can _not_ be done speculatively? - //writing to memory - //mark own speculative events as non-speculative ?? - //create nested speculation ???? - - -//how to resolve speculation? - //check my own entry in a table (and free it!) - - - - diff --git a/run b/run deleted file mode 100755 index bce31cd1..00000000 --- a/run +++ /dev/null @@ -1,3 +0,0 @@ -SCRIPT=$(basename $(test -L "$0" && readlink "$0" || echo "$0")); -SCRIPTPATH=$(cd $(dirname "$0") && pwd); -java -jar $SCRIPTPATH/target/scala-2.13/pdsl.jar "$@" \ No newline at end of file diff --git a/run-build b/run-build deleted file mode 100755 index 29ba5569..00000000 --- a/run-build +++ /dev/null @@ -1,2 +0,0 @@ -sbt assembly -source run \ No newline at end of file diff --git a/semantics/concurrent/Makefile b/semantics/concurrent/Makefile deleted file mode 100644 index 380ea6fe..00000000 --- a/semantics/concurrent/Makefile +++ /dev/null @@ -1,9 +0,0 @@ -all: semantics.pdf - -semantics.pdf: semantics.tex - TEXINPUTS=".:../latex-pl-syntax/:" pdflatex semantics.tex - -clean: phony - rm -rf *.pdf *.aux *.log - -.PHONY: phony diff --git a/semantics/concurrent/semantics.tex b/semantics/concurrent/semantics.tex deleted file mode 100644 index c0208c27..00000000 --- a/semantics/concurrent/semantics.tex +++ /dev/null @@ -1,262 +0,0 @@ -\documentclass{article} -\usepackage{amsmath} -\usepackage{mathpartir} -\usepackage{ttquot} -\usepackage{pl-syntax} -\newcommand{\step}[0]{\ensuremath{\rightarrow}} -\newcommand{\bstep}[0]{\ensuremath{\Downarrow}} -\newcommand{\pstep}[0]{\ensuremath{\rightarrow_{\mathcal{S}}}} -\newcommand{\skips}[0]{~\textsf{skip}~} -\newcommand{\outputs}[0]{~\textsf{output}~} -\newcommand{\spawns}[0]{~\textsf{spawn}~} -\newcommand{\bop}{~\textsf{bop}~} -\newcommand{\uop}{~\textsf{uop}~} -\makeatletter -\newcommand{\conf}[1]{\langle #1\@confx} -\newcommand\@confx{\@ifnextchar\stopconf{\@confend}{\@confi}} -\newcommand\@confend[1]{\rangle} -\newcommand\@confi[1]{,#1 \@confx} -\makeatother - -\begin{document} - -\title{Concurrent Semantics for Pipeline DSL} -\author{Drew Zagieboylo} -\maketitle - -It may be better to not define a new semantics - how about -we just use CHP (communicating sequential processes - https://avlsi.csl.yale.edu/act/doku.php?id=language:langs:chp). - -The main features we care about in CHP are parallel composition ($\parallel$), sequential composition ($;$), -send ($C!V$), receive ($C?V$) and guarded execution ($@[G_1 \implies B_1 ... G_N \implies B_N]$) -where $G$ are guards and $B$ are programs. - -\section{MetaVariables} -\begin{align*} - \begin{array}{lc} - \mbox{Integers} & n \\ - \mbox{Variables} & v,f\\ - \mbox{Expressions} & e\\ - \mbox{Statements} & c\\ - \mbox{Functions} & \mathcal{F}\\ - \mbox{Objects} & \mathcal{O}\\ - \end{array} -\end{align*} - -Here is the intuition behind the syntax of this intermediate representation:\newline -Program: - -List of Module Definition and Module Instantiations w/ Initial Conditions\newline -Module: - -List of Stages, List of Locks, List of Formal Parameters (used to set initial conditions)\newline -Lock: - -A special lock object with a few methods (acquire(), release(), reserve())\newline -Stage: - -A set of receive statements, a sequential program generating combinational assignments, -and a set of guarded send statements\newline - -TODOs: -\begin{itemize} -\item Make the data along channels be "Values" rather than just numbers, since -we will actually be sending records along channels and reading out records into multiple variables. -\item Make "pred" (a.k.a. receives) conditional as well. This is tricky; since we haven't -received yet, we don't have any data that tells us whether or not to execute the receive. -Maybe we allow for conditional receives as commands? That makes things pretty ugly. -\item In general, I'm not super happy with how the communication semantics work right now; -need to clean them up. -\item Include Locks - they probably fit best as a different kind of channel; -so "succ" contains ``Lock.acquire()'' and "pred" contains ``Lock.release'' and -``Lock.reserve()''. See the point on conditional receives for handling the issue -of acquiring locks only if we need to. -\end{itemize} - -\begin{figure}[h] -\begin{syntax} - \abstractCategory[Variables]{v, x, z} - \abstractCategory[Arrays]{v[], x[], z[]} - \abstractCategory[Integers]{n, m} - \abstractCategory[Locks]{L} - \abstractCategory[Channels]{C} - - \category[Programs]{P} - \alternative{ \{ List(M), List(v \mapsto n) \}} %Set of module declarations, Set of module instantiations, Set of Initial Conditions for each instantiated module - - \category[Modules]{M} - \alternative{ \{List(S), List("Mem"), List(v)\}} %List of stages, first element is root stage; List of Locks; List of formal parameters set by initial conditions - - \category[Memories]{"mem"} - \alternative{ \{L, v[]\}} - - \category[Stages]{S} - \alternative{ \{List("pred"), "com", List("succ") \}} - - \category[Expressions]{e} - \alternative{ e " binop " e } - \alternativeLine{ " unop " e } - \alternativeLine{ e " ? " e " : " e } - \alternativeLine{ v } - \alternative{ n } - \alternative{ b } - - \category[Predecessors]{"pred"} - \alternative{ v = "recv " C } - - \category[Commands]{"com"} - \alternative{ "skip" } - \alternative{ "com " ; " com" } - \alternative{ v = e } - \alternativeLine{ L".acquire()"} - \alternative{ L".release()"} - \alternative{ L".reserve()"} - - \category[Successors]{"succ"} - \alternative{ "if ("v") send(" v, C")" } - \alternative{ "if ("v") read mem("v")" } - \alternative{ "if ("v") write mem("v, v")" } - -\end{syntax} -\end{figure} -\section{Notes} - -This language consists of a DAG of pipeline stages. -Every cycle, each stage will, in parallel, check their -predecessors for data. This is analagous to the idea -that registers and ready-valid transactions occur at the beginning -of clock boundaries, thus making the data available right away. -Then, all stages will, in parallel, execute combinational circuits -to compute output values and output guards. The values will -be sent along channels to successors and the guards will determine -which successors have data sent to them. -Then, each stage will, in parallel, send data along -the appropriate successor channels, iff it has received -data from all of its predecessors. If there is any predecessor -from which it hasn't received data, the sends will be skipped. -In the next cycle, this process will repeat except that stages -will remember which channels they have already received from and -will not receive from them again in the next cycle, until they -have sent data out on all expected channels. - -Additionally, this language has a notion of locks or barriers, -which provide further requirements before a stage can send data. -For instance, some stage may execute acquire a lock -on a memory and then also send a request to read that memory. -Or it may simply acquire the lock without reading the memory. -They are separate notions in the semantics. - -TODO:add these to the semantics and figure out if they should -be commands in the second phase of execution or extra guards in the send phase. - -\begin{figure} - \[\begin{array}{r|l} \hline - \text{Variable Mappings} & \Sigma: S \rightarrow \sigma \\ - \text{State Variable Mappings} & \sigma: v \rightarrow n \\ - \text{Receive Status} & \Pi: S \rightarrow \pi \\ - \text{State Receive Status} & \pi: C \rightarrow b \\ - \text{Send Status} & \Delta: S \rightarrow \delta \\ - \text{State Send Status} & \delta: (C + "mem") \rightarrow b \\ \hline - \end{array}\] - \caption{Environment Types} -\end{figure} - -\section{Operational Semantics} -Expression Semantics -\begin{mathpar} - \inferrule*[Left={Uop}]{\conf{\sigma}{e}\stopconf \bstep n' \\ \uop n' = n''} - {\conf{\sigma}{\uop n}\stopconf \bstep n''}\\ - \inferrule*[Left={Binop}]{\conf{\sigma}{e_1}\stopconf \bstep n \\ \conf{\sigma}{e_2}\stopconf \bstep n' \\ n \bop n' = n''} - {\conf{\sigma}{e_1 \bop e_2}\stopconf \bstep n''}\\ - \inferrule*[Left={Int-Lookup}]{\sigma(v) = n}{\conf{\sigma}{v}\stopconf \bstep n}\\ - \inferrule*[Left={Ternary}]{\conf{\sigma}{e_b}\stopconf \bstep n_c \\ \conf{\sigma}{e_t}\stopconf \bstep n_t \\ - \conf{\sigma}{e_f}\stopconf \bstep n_f \\ n_c \neq 0 " ? " n_t " : " n_f} - {\conf{\sigma}{e_b " ? " e_t " : " e_f}\stopconf \bstep n}\\ -\end{mathpar} -Receive Semantics -\begin{mathpar} - \inferrule*[Left={Block-Recv}]{ C.isEmpty() " or " \pi(C) = "true"} - {\conf{\sigma}{\pi}{v = "recv " C}\stopconf \step \conf{\sigma}{\pi}\stopconf}\\ - \inferrule*[Left={Accept-Recv}]{!C.isEmpty() \\ \pi(C) = "false" \\ \sigma' = \sigma[v \mapsto C.peek()] \\ - \pi' = \pi[C \mapsto "true"]} - {\conf{\sigma}{v = "recv " C}\stopconf \step \conf{\sigma'}{\pi'}\stopconf}\\ - \inferrule*[Left={Recv-List}]{ - \mathcal{P} = \{"pred"_0..."pred"_n\} \\ - \forall p \in \mathcal{P}. \conf{\sigma}{\pi}{p}\stopconf \step \conf{\sigma_p'}{\pi_p'}\stopconf \\ - \sigma' = \bigcup_{p \in \mathcal{P}} \sigma_p' \\ \pi' = \bigcup_{p \in \mathcal{P}} \pi_p'} - {\conf{\sigma}{\pi}{\mathcal{P}}\stopconf \step \conf{\sigma'}{\pi'}\stopconf}\\ -\end{mathpar} - -Command Semantics -\begin{mathpar} - \inferrule*[Left={Seq-Skip}]{ } - {\conf{\sigma}{\skips ; "com"_2}\stopconf \step \conf{\sigma}{"com"_2}\stopconf}\\ - \inferrule*[Left={Seq}]{ \conf{\sigma}{"com"_1}\stopconf \step \conf{\sigma'}{"com"_1'}\stopconf} - {\conf{\sigma}{"com"_1" ; com"_2}\stopconf \step \conf{\sigma'}{"com"_1'" ; com"_2}\stopconf}\\ - \inferrule*[Left={Assign}]{ v \not\in "dom"(\sigma) \\ \conf{\sigma}{e}\stopconf \bstep n \\ \sigma' = \sigma[v \mapsto n]} - {\conf{\sigma}{v = e}\stopconf \step \conf{\sigma'}{\skips}\stopconf}\\ -\end{mathpar} -Send Semantics -\begin{mathpar} -% \boxed{\conf{\sigma}{\delta}{"if ("v_g") send(" v_v, C")"}\stopconf -% \step \conf{\delta'}\stopconf}\\ - \inferrule*[Left={-Guard-False}]{ \sigma(v_g) = 0 \\ \delta' = \delta[C \mapsto "true"]} - {\conf{\sigma}{\delta}{"if ("v_g")" ...}\stopconf \step \conf{\delta}\stopconf}\\ - \inferrule*[Left={Send-Blocked}]{ \sigma(v_g) \neq 0 \\ C.isFull() " or " \delta(C) = "true"} - {\conf{\sigma}{\delta}{"if ("v_g" send(" v_v, C")"}\stopconf \step \conf{\delta}\stopconf}\\ - \inferrule*[Left={Send}]{ \sigma(v_g) \neq 0 \\ !C.isFull() \\ \delta(C) = "false" - \\ \delta' = \delta[C \mapsto "true"] \\ C.push(\sigma(v_v))} - {\conf{\sigma}{\delta}{"if ("v_g" send(" v_v, C")"}\stopconf \step \conf{\delta}\stopconf}\\ - \inferrule*[Left={Send-List}] - { \forall c \in "dom"(\pi). \pi(c) = "true" \\ - \mathcal{S} = \{"succ"_0..."succ"_n\} \\ - \forall s \in \mathcal{S}. \conf{\sigma}{\delta}{s}\stopconf \step \conf{\delta_s'}\stopconf \\ - \delta' = \bigcup_{s \in \mathcal{S}} \delta_s' } - {\conf{\sigma}{\pi}{\delta}{\mathcal{S}}\stopconf \step \conf{\delta'}\stopconf}\\ - \inferrule*[Left={Wait-List}] - { \exists c \in "dom"(\pi). \pi(c) = "false" } - {\conf{\sigma}{\pi}{\delta}{\mathcal{S}}\stopconf \step \conf{\delta}\stopconf}\\ -\end{mathpar} - -End of Cycle Semantics -\begin{mathpar} - \inferrule*[Left={Retry}] {\exists c \in "dom"(\delta). \delta(c) = "false" } - {\conf{\pi}{\delta}\stopconf \step \conf{\pi}{\delta}\stopconf} \\ - \inferrule*[Left={Reset}] {\delta = \{c_1 \mapsto "true"...c_n \mapsto "true"\} \\ - \pi = \{C_1 \mapsto "true"...C_n \mapsto "true"\} \\ \forall C_i. C_i.pop() \\ - \pi' = \{C_1 \mapsto "false"...C_n \mapsto "false" \} \\ - \delta' = \{c_1 \mapsto "false"..c_n \mapsto "false"\}} - {\conf{\pi}{\delta}\stopconf \step \conf{\pi'}{\delta'}\stopconf}\\ -\end{mathpar} -Module Semantics -\begin{mathpar} - \inferrule*[Left={Execute-Recvs}]{ - \forall s \in S. \conf{\Sigma(s)}{\Pi(s)}{s."recv"}\stopconf \step - \conf{\sigma_s'}{\pi_s'}\stopconf \\ - \Sigma' = \bigcup_{s\in S} \sigma_s' \\ \Pi' = \bigcup_{s \in S} \pi_s'} - {\conf{\Sigma}{\Pi}{\Delta}{List(S)}\stopconf \step - \conf{\Sigma'}{\Pi'}{\Delta}{\{List(S), "exec"\}}\stopconf} \\ - \inferrule*[Left={Execute-Commands}]{\forall s \in S. \conf{\Sigma(s)}{s."com"}\stopconf \step^* - \conf{\sigma_s'}{\skips}\stopconf \\ \forall s \in S. \Sigma'[s \mapsto \sigma_s']} - {\conf{\Sigma}{\Pi}{\Delta}{\{List(S), "exec"\}}\stopconf \step - \conf{\Sigma'}{\Pi}{\Delta}{\{List(S), "send"\}}\stopconf}\\ - \inferrule*[Left={Execute-Sends}]{\forall s \in S. \conf{\Sigma(s)}{\Pi(s)}{\Delta(s)}{s."send"}\stopconf \step - \conf{\delta_s'}\stopconf \\ \Delta' = \bigcup_{s \in S} \delta_s'} - {\conf{\Sigma}{\Pi}{\Delta}{\{List(S),"send"\}}\stopconf \step - \conf{\Sigma}{\Pi}{\Delta'}{\{List(S), "endcycle"\}}\stopconf}\\ - \inferrule*[Left={End-Cycles}]{ \forall s \in S. \conf{\Pi(s)}{\Delta(s)}\stopconf \step - \conf{\pi_s'}{\delta_s'}\stopconf \\ \Pi' = \bigcup_{s \in S} \pi_s' \\ \Delta' = \bigcup_{s \in S} \delta_s' } - {\conf{\Sigma}{\Pi}{\Delta}{\{List(S), "endcycle"\}}\stopconf \step - \conf{\emptyset}{\Pi'}{\Delta'}{\{List(S), "recv"\}}\stopconf}\\ -\end{mathpar} -\end{document} - - -In this semantics, each module is comprised of a set of stages. -In each cycle, every stage will, in parallel, check for inputs for validity -and outputs for readiness. If all of its inputs are ready, then it -will compute the values of its outpus and send any which are ready this cycle. -Every cycle, this procedure is repeated until all outputs have been sent. -On the cycle when a stage has sent all of its outputs, it will mark its -inputs as used (by popping them off of its input queues) and none -of its outputs as sent. diff --git a/semantics/concurrent/ttquot.sty b/semantics/concurrent/ttquot.sty deleted file mode 100644 index a740e20b..00000000 --- a/semantics/concurrent/ttquot.sty +++ /dev/null @@ -1,180 +0,0 @@ -\NeedsTeXFormat{LaTeX2e}[2.09] -\ProvidesPackage{ttquot} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% ttquot.sty -% -% Simple markdown support for LaTeX. (It was developed in 1992 before -% "markdown" existed!) -% -% One of the most common problems is switching conveniently into the -% typewriter font and back. This style file makes the ordinary double -% quotation mark (") serve this function. Note that the meaning of \tt -% may be different in math and text mode, for example if the "times" -% package is being used. -% -% This package also makes underscore characters (_) switch into -% emphasized mode and back, unless inside " quotes or in math mode. This -% makes ordinary variable names easier to type in typewriter font, and -% makes emphasized mode obey a common ASCII text convention. -% -% Options: -% sfcode -% Makes text inside quotation marks come out in \sf font. -% small -% Makes text inside quotation marks come out \small (except in math -% mode.) This is especially useful when using the times package, because -% the Courier and Helvetica fonts are larger than Times. -% stdbraces -% By default, the commands \{ and \} emit ordinary characters 123 and -% 125 inside quotation marks. This works well if you are in \tt font, -% but not so well in a font (e.g., \sf) lacking these characters. Use -% stdbraces to defeat it. -% bfemph -% Make underscore turn on boldface instead of italics. -% -% The following macros are defined and may be used or overridden. -% -% \ttquot@activate Turn on ttquot processing. On by default. -% \ttquot@deactivate Turn off ttquot processing. -% \ttquot@ttmode The 'code' environment introduced by " -% \ttquot@emmode The 'emphasized' environment introduced by _ -% \ttquot@setup Commands that are emitted in the " environment. -% \ttquot@ttfont The font part of tt@setup, By default, \tt. -% \ttquot@ttsize The font size part of tt@setup, By default, nothing. -% \ttquot@emfont The commands that are emitted in the _ environment. -% By default, \em -% \ttquot@braces Another command emitted in the " environment. -% By default, changes braces to use tt font chars. -% The "stdbraces" option defeats this. -% \ttquot@mark Always represents the plain character (") -% \ttquot@us Represents the original meaning of (_) -% -% This style file is maintained by Andrew Myers (andru@cs.cornell.edu) -% -% Change log: -% Fri Nov 6 14:35:49 EST 1992 Added this documentation andru -% Tue Nov 10 23:05:44 EST 1992 Changed underscore to do \em andru -% Wed Nov 11 17:00:00 EST 1992 Fixed various bugs, added * andru -% Tue Feb 16 23:48:20 EST 1993 Fixed "number" bug, added \* andru -% Tue Mar 23 13:39:39 EST 1993 Got rid of a little cruft andru -% Tue Apr 26 16:07:18 EDT 1994 Made _ work in other fonts andru -% Wed Oct 12 17:39:49 EDT 1994 Made activate/deactivate work andru -% Wed Feb 08 15:00:31 EST 1995 Made * work again andru -% Wed Jun 7 18:08:23 EDT 1995 Got rid of * andru -% Sun Aug 4 15:58:16 EDT 2002 Rewrite using environments Robert Grimm -% Thu Aug 15 11:39:12 EDT 2002 More documentation andru -% Mon Sep 26 08:14:21 EDT 2016 \protect quotes in captions andru -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Options -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\DeclareOption{sfcode}{\def\ttquot@ttfont{\sf}} -\DeclareOption{small}{\def\ttquot@ttsize{\ifmmode\else\small\fi}} -\DeclareOption{stdbraces}{\def\ttquot@braces{}} -\DeclareOption{bfemph}{\def\ttquot@emfont{\bf}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Save original definitions -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\let\ttquot@mark="% Catch original definition of quotation mark -\let\ttquot@us=_% Catch original definition of underscore - -\def\ttquot@tt@us{\char95} % how to render underscore in tt mode. - -% Change character codes to make them active temporarily. -\catcode`\"=\active% -\catcode`\_=\active% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Change " to place its contents inside {\ttquot@ttfont ... } -% Also, underscores are underscores, not subscripts -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newenvironment{ttquot@ttmode}{% -\mbox\bgroup% -\ttquot@setup% -\def_{\ifmmode\ttquot@us\else\ttquot@tt@us\fi}% -\def"{\protect\end{ttquot@ttmode}}% -}% -{\egroup} - -\def\ttquot@setup{\ttquot@ttfont\ttquot@ttsize\ttquot@braces} - -\def\ttquot@ttfont{\ttfamily} -\def\ttquot@braces{\def\{{\char123}\def\}{\char125}} -\def\ttquot@ttsize{} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Change _ to place its contents inside {\ttquot@emfont ... } -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newenvironment{ttquot@emmode}{% -\ttquot@emfont% -\def_{\protect\end{ttquot@emmode}}% -}% -{} - -\gdef\ttquot@emfont{\em} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Change LaTeX's verbatim mode to use \ttquot@ttfont -% instead of \tt; also, do right thing with _ -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\def\@verbatim{\trivlist \item[]\if@minipage\else\vskip\parskip\fi -\leftskip\@totalleftmargin\rightskip\z@ -\parindent\z@\parfillskip\@flushglue\parskip\z@ -\@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par} -\obeylines \ttquot@ttfont -\@noligs \let\do\@makeother \dospecials -\catcode`\_=13% -\def_{\_}% -\catcode``=13% -} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Macros to turn the package on and off -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\gdef\ttquot@activate{% -\catcode`\"=\active% -\catcode`\_=\active% -\def"{\protect\begin{ttquot@ttmode}}% -\def_{\ifmmode\ttquot@us\else\protect\begin{ttquot@emmode}\fi}% -} - -\gdef\ttquot@deactivate{% -\def"{\ttquot@mark}% -\def_{\ttquot@us}% -\catcode`\"=12% -\catcode`\_=8% -} - -% Restore character codes to avoid messing up other packages. -% Character codes will be turned back on at beginning of document. -\catcode`\"=12 -\catcode`\_=8 - -\let\ttquot@old@citex\@citex - -\def\@citex[#1]#2{ - \edef\ttquot@us@catcode{\the\catcode`\_}% - \catcode`\_=13% - \ttquot@old@citex[#1]#2 - \catcode`\_=\ttquot@us@catcode\relax} - -\let\ttquot@old@bibliography\bibliography - -\def\bibliography#1{% - \catcode`\_=8 - \ttquot@old@bibliography{#1}} - -\ProcessOptions -\AtBeginDocument{\ttquot@activate} diff --git a/semantics/latex-pl-syntax/.gitignore b/semantics/latex-pl-syntax/.gitignore deleted file mode 100644 index 1a83c068..00000000 --- a/semantics/latex-pl-syntax/.gitignore +++ /dev/null @@ -1,244 +0,0 @@ -*.pdf - -## Core latex/pdflatex auxiliary files: -*.aux -*.lof -*.log -*.lot -*.fls -*.out -*.toc -*.fmt -*.fot -*.cb -*.cb2 -.*.lb - -## Intermediate documents: -*.dvi -*.xdv -*-converted-to.* -# these rules might exclude image files for figures etc. -# *.ps -# *.eps -# *.pdf - -## Generated if empty string is given at "Please type another file name for output:" -.pdf - -## Bibliography auxiliary files (bibtex/biblatex/biber): -*.bbl -*.bcf -*.blg -*-blx.aux -*-blx.bib -*.run.xml - -## Build tool auxiliary files: -*.fdb_latexmk -*.synctex -*.synctex(busy) -*.synctex.gz -*.synctex.gz(busy) -*.pdfsync - -## Auxiliary and intermediate files from other packages: -# algorithms -*.alg -*.loa - -# achemso -acs-*.bib - -# amsthm -*.thm - -# beamer -*.nav -*.pre -*.snm -*.vrb - -# changes -*.soc - -# cprotect -*.cpt - -# elsarticle (documentclass of Elsevier journals) -*.spl - -# endnotes -*.ent - -# fixme -*.lox - -# feynmf/feynmp -*.mf -*.mp -*.t[1-9] -*.t[1-9][0-9] -*.tfm - -#(r)(e)ledmac/(r)(e)ledpar -*.end -*.?end -*.[1-9] -*.[1-9][0-9] -*.[1-9][0-9][0-9] -*.[1-9]R -*.[1-9][0-9]R -*.[1-9][0-9][0-9]R -*.eledsec[1-9] -*.eledsec[1-9]R -*.eledsec[1-9][0-9] -*.eledsec[1-9][0-9]R -*.eledsec[1-9][0-9][0-9] -*.eledsec[1-9][0-9][0-9]R - -# glossaries -*.acn -*.acr -*.glg -*.glo -*.gls -*.glsdefs - -# gnuplottex -*-gnuplottex-* - -# gregoriotex -*.gaux -*.gtex - -# htlatex -*.4ct -*.4tc -*.idv -*.lg -*.trc -*.xref - -# hyperref -*.brf - -# knitr -*-concordance.tex -# TODO Comment the next line if you want to keep your tikz graphics files -*.tikz -*-tikzDictionary - -# listings -*.lol - -# makeidx -*.idx -*.ilg -*.ind -*.ist - -# minitoc -*.maf -*.mlf -*.mlt -*.mtc[0-9]* -*.slf[0-9]* -*.slt[0-9]* -*.stc[0-9]* - -# minted -_minted* -*.pyg - -# morewrites -*.mw - -# nomencl -*.nlg -*.nlo -*.nls - -# pax -*.pax - -# pdfpcnotes -*.pdfpc - -# sagetex -*.sagetex.sage -*.sagetex.py -*.sagetex.scmd - -# scrwfile -*.wrt - -# sympy -*.sout -*.sympy -sympy-plots-for-*.tex/ - -# pdfcomment -*.upa -*.upb - -# pythontex -*.pytxcode -pythontex-files-*/ - -# thmtools -*.loe - -# TikZ & PGF -*.dpth -*.md5 -*.auxlock - -# todonotes -*.tdo - -# easy-todo -*.lod - -# xmpincl -*.xmpi - -# xindy -*.xdy - -# xypic precompiled matrices -*.xyc - -# endfloat -*.ttt -*.fff - -# Latexian -TSWLatexianTemp* - -## Editors: -# WinEdt -*.bak -*.sav - -# Texpad -.texpadtmp - -# Kile -*.backup - -# KBibTeX -*~[0-9]* - -# auto folder when using emacs and auctex -./auto/* -*.el - -# expex forward references with \gathertags -*-tags.tex - -# standalone packages -*.sta - -# generated if using elsarticle.cls -*.spl diff --git a/semantics/latex-pl-syntax/LICENSE b/semantics/latex-pl-syntax/LICENSE deleted file mode 100644 index 67e00fe2..00000000 --- a/semantics/latex-pl-syntax/LICENSE +++ /dev/null @@ -1,21 +0,0 @@ -MIT License - -Copyright (c) 2019 Andrew Hirsch, Josh Acay - -Permission is hereby granted, free of charge, to any person obtaining a copy -of this software and associated documentation files (the "Software"), to deal -in the Software without restriction, including without limitation the rights -to use, copy, modify, merge, publish, distribute, sublicense, and/or sell -copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all -copies or substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, -FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE -AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER -LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, -OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE -SOFTWARE. diff --git a/semantics/latex-pl-syntax/README.md b/semantics/latex-pl-syntax/README.md deleted file mode 100644 index 48eeb538..00000000 --- a/semantics/latex-pl-syntax/README.md +++ /dev/null @@ -1,5 +0,0 @@ - # `pl-syntax` - - This is a LaTeX package for defining the abstract syntax of programming languages. - - See `example.tex` to learn how to use this package. diff --git a/semantics/latex-pl-syntax/example.tex b/semantics/latex-pl-syntax/example.tex deleted file mode 100644 index 39748d38..00000000 --- a/semantics/latex-pl-syntax/example.tex +++ /dev/null @@ -1,57 +0,0 @@ -\documentclass{article} - -\usepackage{pl-syntax} - - -\title{Example Usage of \texttt{pl-syntax} Package} -\author{Andrew Hirsch \and Josh Acay} - - -\begin{document} -\maketitle - -\section{The Simply Typed Lambda Calculus} - -Read the comments in the \texttt{.tex} source for an explanation of how -the following is generated. - -\begin{figure}[h] - \begin{syntax} - % Define a syntactic category with no right-hand side. - \abstractCategory[Variables]{x, y, z} - - % Start a category definition. Optional input is the category - % description, the other declares the meta variable(s) you will - % use to refer to this category. - \category[Expressions]{e} - % Each alternative is introduces in a new line. - \alternative{x} - \alternative{\lambda x . e} - \alternative{e_1 e_2} - - \category[Values]{v} - \alternative{\lambda x . e} - - % You can add vertical spacing between categories to visually group them. - \separate - % You can pass the amount of space explicitly if you want to manually control it: - % \separate[5ex] - - \category[Types]{\tau} - \alternative{\mathbf{Nat}} - % You can place alternatives on a new line. - \alternativeLine{\tau_1 \rightarrow \tau_2} - - \category[Contexts]{\Gamma} - \alternative{x_1 : \tau_1, \ldots, x_n : \tau_n} - % You can use words to describe more complicated properties of - % definitions if you don't want to use BNF. - \note{no repeats} - \note{unordered} - \end{syntax} - - \caption{Terms and Types of the Simply Typed Lambda Calculus} - \label{fig:abstract-syntax} -\end{figure} - -\end{document} diff --git a/semantics/latex-pl-syntax/pl-syntax.sty b/semantics/latex-pl-syntax/pl-syntax.sty deleted file mode 100644 index 12f8329c..00000000 --- a/semantics/latex-pl-syntax/pl-syntax.sty +++ /dev/null @@ -1,49 +0,0 @@ -\NeedsTeXFormat{LaTeX2e} -\ProvidesPackage{pl-syntax} - [2019/04/22 version 1.0.0 Abstract Syntax Definitions for Programming Languages] - -% Suppresses row breaks when set to true. Used to prevent unnecessary -% line breaks that would otherwise be generated by default. -\newif\if@syntax@suppressNewRow - -% Whether we have encountered the first alternative in a category -% definition or not. Used to suppress a leading separator. -\newif\if@syntax@firstAlternative - -% Define the abstract syntax of a programming language. -\newenvironment{syntax} -{% - % Define a new syntactic category (e.g. expressions, statements). - \newcommand{\category}[2][]{% - \@newRow \textrm{##1} & ##2 & ::= &% - \@syntax@firstAlternativetrue% - }% - % A category with no right-hand side. This allows you to name meta - % variables without defining the syntactic category explicitly. - \newcommand{\abstractCategory}[2][]{% - \@newRow \textrm{##1} & ##2% - \@syntax@firstAlternativetrue% - }% - % Define a new alternative for the most recent category. - \newcommand{\alternative}[1]{% - \@alt ##1% - \@syntax@firstAlternativefalse% - }% - % Like `alternative`, but places the clause on a new line. - \newcommand{\alternativeLine}[1]{% - \@newRow & & \@alt & ##1% - \@syntax@firstAlternativefalse% - }% - % Add extra information to the most recently declared alternative. - % For example, you can use this to note that the context is unordered. - \newcommand{\note}[1]{\@newRow & & & (\textrm{##1})}% - % Add vertical space between declarations. - \newcommand{\separate}[1][1ex]{\\[##1]\@syntax@suppressNewRowtrue} - % Symbol used between alternatives. - \newcommand{\@alt}{\if@syntax@firstAlternative \else \,\mid\, \fi} - % Start a new row. - \newcommand{\@newRow}{\if@syntax@suppressNewRow \@syntax@suppressNewRowfalse \else \\ \fi} -% - \[\begin{array}{llcl}\@syntax@suppressNewRowtrue\ignorespaces% -} -{\end{array}\]\ignorespacesafterend} \ No newline at end of file diff --git a/semantics/sequential/Makefile b/semantics/sequential/Makefile deleted file mode 100644 index 380ea6fe..00000000 --- a/semantics/sequential/Makefile +++ /dev/null @@ -1,9 +0,0 @@ -all: semantics.pdf - -semantics.pdf: semantics.tex - TEXINPUTS=".:../latex-pl-syntax/:" pdflatex semantics.tex - -clean: phony - rm -rf *.pdf *.aux *.log - -.PHONY: phony diff --git a/semantics/sequential/semantics.synctex(busy) b/semantics/sequential/semantics.synctex(busy) deleted file mode 100644 index e69de29b..00000000 diff --git a/semantics/sequential/semantics.tex b/semantics/sequential/semantics.tex deleted file mode 100644 index 598dc421..00000000 --- a/semantics/sequential/semantics.tex +++ /dev/null @@ -1,192 +0,0 @@ -\documentclass{article} -\usepackage{amsmath} -\usepackage{mathpartir} -\usepackage{ttquot} -\usepackage{pl-syntax} - -\providecommand{\absint}[1]{\left \lfloor #1 \right \rfloor } -\newcommand{\step}[0]{\ensuremath{\rightarrow}} -\newcommand{\bstep}[0]{\ensuremath{\Downarrow}} -\newcommand{\pstep}[0]{\ensuremath{\rightarrow_{\mathcal{S}}}} -\newcommand{\skips}[0]{~\textsf{skip}~} -\newcommand{\outputs}[0]{~\textsf{output}~} -\newcommand{\spawns}[0]{~\textsf{spawn}~} -\newcommand{\locks}[0]{~\textsf{wait-for-lock}~} -\newcommand{\bypass}[0]{~\textsf{bypass}~} -\newcommand{\bop}{~\textsf{bop}~} -\newcommand{\uop}{~\textsf{uop}~} -\newcommand{\tdash}{\ensuremath{---}} -\makeatletter -\newcommand{\conf}[1]{\langle #1\@confx} -\newcommand\@confx{\@ifnextchar\stopconf{\@confend}{\@confi}} -\newcommand\@confend[1]{\rangle} -\newcommand\@confi[1]{,#1 \@confx} -\makeatother - -\begin{document} - -\title{Sequential Semantics for Pipeline DSL} -\author{Drew Zagieboylo} -\maketitle - -\section{MetaVariables} -\begin{align*} - \begin{array}{lc} - \mbox{Integers} & n \\ - \mbox{Variables} & v,f\\ - \mbox{Expressions} & e\\ - \mbox{Statements} & c\\ - \mbox{Functions} & \mathcal{F}\\ - \mbox{Objects} & \mathcal{O}\\ - \end{array} -\end{align*} - -\section{Type System} - -The type system is used to enforce a number of constraints -that will ensure compilation of the program to a concurrent -system maintains correctness. This involves typechecking -a few different sets of rules: - -\begin{itemize} -\item Base Types - Normal types for circuits like sized integers and booleans. - We have a very limited notion of base types, like a subset of FIRRTL. This is mostly - uninteresting. -\item Operation Timing - We have both synchronous (combinational) and asynchronous - assignment. The latter is used to access arrays and external modules and the results - of such operations take time to become available. We ensure that all variable - accesses occur once their data has been made available (via logical the time-step operation '---'). - This is also relatively uninteresting. -\item Lock Acquisition - A key mechanism for ensuring correctness is ensuring - that stateful operations (like writing to memories) happen in order. We ensure - this order by forcing memory-accessing operations to happen only after the associated - lock has been acquired. A secondary requirement of this check is that locks are - acquired in-order; we enforce this by ensuring that there is exactly one point - in the pipeline at which locks are acquired. This requirement can be relaxed with - non-blocking acquisition (which we call reservation) that can happen in-order without - forcing early pipeline stalls waiting for a lock that won't be needed until later. -\item Speculation - Speculation introduces some complexity and we must also - prevent speculative code from executing any irreversible operations (such as - modifying memory). However, speculative code *can* acquire and free locks, - in certain cases. This checker ensures that all of those happen appropriately. -\end{itemize} - -\begin{figure}[h] - \begin{syntax} - \abstractCategory[Variables]{v, x, z} - \abstractCategory[Command]{c} - \abstractCategory[Memory]{m} - \abstractCategory[Pipeline Module]{\mathcal{P}} - \category[LockState]{s} - \alternative{"free"} - \alternative{"reserved"} - \alternative{"acquired"} - \alternative{"released"} - \category[LockReservationMap]{\mathcal{L}} - \alternative{ m_1 \mapsto s_; m_2 \mapsto s_2;...;m_n \mapsto s_n } - \category[LockMap]{L} - \alternative{ m_1 \mapsto s_1; m_2 \mapsto s_2;...;m_n \mapsto s_n } - \end{syntax} -\end{figure} - -\subsection{Lock Reservation Regions} - -\begin{mathpar} - - \mathcal{L}^1 " merge " \mathcal{L}^2 = \{ \forall m. m \mapsto s | s = - \begin{cases} - \mathcal{L}^1(m) & \mathcal{L}^1(m) = \mathcal{L}^2(m)\\ - "released" & \mathcal{L}^1(m) = "free" || \mathcal{L}^2(m) = "free"\\ - UNDEFINED & - \end{cases}\}\\ - - \boxed{ \mathcal{L} \vdash c \dashv \mathcal{L}'}\\ - - \inferrule*[Left=StartRes]{ \mathcal{L}(m) = "free" \\ \mathcal{L}' = \mathcal{L}[m \mapsto "acquired"] } - { \mathcal{L} \vdash "start"(m) \dashv \mathcal{L}' }\\ - \inferrule*[Left=EndRes]{ \mathcal{L}(m) = "acquired" \\ \mathcal{L}' = \mathcal{L}[m \mapsto "released"] } - { \mathcal{L} \vdash "end"(m) \dashv \mathcal{L}' }\\ - \inferrule*[Left=ResOp]{ "loc" = m[x] || m \\ \mathcal{L}(m) = "acquired" } - { \mathcal{L} \vdash reserve("loc") \dashv \mathcal{L} }\\ - \inferrule*[Left=If] { \forall i \in \{t, f\}. \mathcal{L} \vdash c_i \dashv \mathcal{L}^i \\ - \mathcal{L}' = \mathcal{L}^t " merge " \mathcal{L}^f \\ - \forall m. \mathcal{L}^t(m) = "released" \implies \mathcal{L}(m) = "acquired" || \mathcal{L}^f(m) = "free" \\ - \forall m. \mathcal{L}^f(m) = "released" \implies \mathcal{L}(m) = "acquired" || \mathcal{L}^t(m) = "free"} - { \mathcal{L} \vdash "if " (c) " then " c_t " else " c_f \dashv \mathcal{L}'} - - \inferrule*[Left=AllReleased] { \forall m. \mathcal{L}(m) = "free" \\ \forall m. \mathcal{L}'(m) \in \{"free", "released"\}} - { \mathcal{L} \vdash \mathcal{P} \dashv \mathcal{L}'} -\end{mathpar} - -Lock reservation ensures that address-specific locks can be acquired over multiple -cycles while maintaining the correct reservation order. -These regions represent mutual exclusion sections and -prevent multiple threads from executing those regions of the pipeline in parallel. -Typically "start" and "end" should be placed in the same cycle to prevent runtime overhead. -Since "if" statements imply potential out-of-order execution the lock region for a given -memory can only start in at most one of the branches. However, lock regions can start outside -of "if" statements and be ended in each branch separately. The last rule ensures that all -modules typecheck assuming that all lock regions are currently free and at the end -of execution it must have released any lock regions that it acquired. - -\subsection{Lock Acquisition} - -All lock reservation must occur in one of the aforementioned reservation regions. -These rules ensure that all lock operations occur on locks that are in appropriate -states but do not need to check the lock reservation region status. - - -\begin{mathpar} - \boxed{L \vdash c \dashv L'}\\ - \inferrule*[Left=MemRead]{ \mathcal{B} \implies L(m[x]) = "acquired"} - { \mathcal{B}, L \vdash m[x] \leftarrow v \dashv \mathcal{B}, L }\\ - \inferrule*[Left=MemWrite]{ \mathcal{B} \implies L(m[x]) = "acquired"} - { \mathcal{B}, L \vdash v \leftarrow m[x] \dashv \mathcal{B}, L }\\ - \inferrule*[Left=Reserve]{ \mathcal{B} \implies L(m[x]) = "free"} - {\mathcal{B}, L \vdash "reserve"(m[x]) \dashv \mathcal{B}, L[m[x] \mapsto "reserved"] }\\ - \inferrule*[Left=Acquire]{ \mathcal{B} \implies L(m[x]) = "reserved"} - {\mathcal{B}, L \vdash "acquire"(m[x]) \dashv \mathcal{B}, L[m[x] \mapsto "acquired"] }\\ - \inferrule*[Left=Free]{ \mathcal{B} \implies L(m[x]) = "acquired" } - {\mathcal{B}, L \vdash "free"(m[x]) \dashv \mathcal{B}, L[m[x] \mapsto "released"]}\\ - \inferrule*[Left=If]{ - \mathcal{B}_t = \mathcal{B} \wedge \absint{e} \\ - \mathcal{B}_f = \mathcal{B} \wedge "not"(\absint{e}) \\ - \mathcal{B}_t , L \vdash c_t \dashv \mathcal{B}_t, L_t \\ - \mathcal{B}_f, L \vdash c_f \dashv \mathcal{B}_f, L_f \\ - L' = \absint{e} " ? " L_t : ("not"(\absint{e}) " ? " L_f " : " L_{\top})} - {\mathcal{B}, L \vdash "if " e " then " c_t " else " c_v \dashv \mathcal{B},L'}\\ -\end{mathpar} - -Locks must have been "acquired" to access the associated memory. Once a lock -is "free"ed, it cannot be acquired again since it is in the "released" state. -Lock acquisition happens in two steps: first the lock is "reserved" which enqueues -a request for the lock; second the lock is "acquired" by blocking until the lock status -says that the reservation is now owned by the current thread. - -The $\mathcal{B}$ predicate tracks an abstraction of the currently valid branch conditions. -$\absint{e}$ is an abstract interpretation of the expression $e$ and is used to restrict or -prove the current state of a given lock. "if" statements create a new Lockstate map -that is represented as a ternary expression. The lookup operation into such a map -requires some predicate (provided by $\mathcal{B}$ in the other commands); if that -predicate proves part of the implication, then the lockstate for the given memory location -is looked up in that lock map. - -_N.B._ The ternary lock map is not a simple if-then-else because $\absint{e}$ is an approximation -and therefore, being unable to prove $\absint{e}$ _does not imply_ $"not"(\absint{e})$. Therefore, -if neither of those can be proven the state is looked up in the ``unknown lock map'', $L_{\top}$. -This map always returns "unknown", or $\top$ as the state of the given lock, which will prevent -any of the lock related commands from typechecking. - - -\begin{mathpar} - \boxed{ L \vdash \mathcal{P} \dashv L' }\\ - \inferrule*[Left={Deadlock-Free}] - {\forall \{m,x\} "true" \implies L(m[x]) = "free" \\ - \forall \{m,x\}. L'(m[x]) \in \{"free", "released"\}} - {"true", L \vdash \mathcal{P} \dashv "true", L'} -\end{mathpar} -Lastly, to avoid deadlock, like lock acquisition regions, -pipeline modules must type check with the assumption that no locks have been acquired, -and after execution all locks must either be "free" or "released" - -\end{document} diff --git a/semantics/sequential/ttquot.sty b/semantics/sequential/ttquot.sty deleted file mode 100644 index a740e20b..00000000 --- a/semantics/sequential/ttquot.sty +++ /dev/null @@ -1,180 +0,0 @@ -\NeedsTeXFormat{LaTeX2e}[2.09] -\ProvidesPackage{ttquot} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% ttquot.sty -% -% Simple markdown support for LaTeX. (It was developed in 1992 before -% "markdown" existed!) -% -% One of the most common problems is switching conveniently into the -% typewriter font and back. This style file makes the ordinary double -% quotation mark (") serve this function. Note that the meaning of \tt -% may be different in math and text mode, for example if the "times" -% package is being used. -% -% This package also makes underscore characters (_) switch into -% emphasized mode and back, unless inside " quotes or in math mode. This -% makes ordinary variable names easier to type in typewriter font, and -% makes emphasized mode obey a common ASCII text convention. -% -% Options: -% sfcode -% Makes text inside quotation marks come out in \sf font. -% small -% Makes text inside quotation marks come out \small (except in math -% mode.) This is especially useful when using the times package, because -% the Courier and Helvetica fonts are larger than Times. -% stdbraces -% By default, the commands \{ and \} emit ordinary characters 123 and -% 125 inside quotation marks. This works well if you are in \tt font, -% but not so well in a font (e.g., \sf) lacking these characters. Use -% stdbraces to defeat it. -% bfemph -% Make underscore turn on boldface instead of italics. -% -% The following macros are defined and may be used or overridden. -% -% \ttquot@activate Turn on ttquot processing. On by default. -% \ttquot@deactivate Turn off ttquot processing. -% \ttquot@ttmode The 'code' environment introduced by " -% \ttquot@emmode The 'emphasized' environment introduced by _ -% \ttquot@setup Commands that are emitted in the " environment. -% \ttquot@ttfont The font part of tt@setup, By default, \tt. -% \ttquot@ttsize The font size part of tt@setup, By default, nothing. -% \ttquot@emfont The commands that are emitted in the _ environment. -% By default, \em -% \ttquot@braces Another command emitted in the " environment. -% By default, changes braces to use tt font chars. -% The "stdbraces" option defeats this. -% \ttquot@mark Always represents the plain character (") -% \ttquot@us Represents the original meaning of (_) -% -% This style file is maintained by Andrew Myers (andru@cs.cornell.edu) -% -% Change log: -% Fri Nov 6 14:35:49 EST 1992 Added this documentation andru -% Tue Nov 10 23:05:44 EST 1992 Changed underscore to do \em andru -% Wed Nov 11 17:00:00 EST 1992 Fixed various bugs, added * andru -% Tue Feb 16 23:48:20 EST 1993 Fixed "number" bug, added \* andru -% Tue Mar 23 13:39:39 EST 1993 Got rid of a little cruft andru -% Tue Apr 26 16:07:18 EDT 1994 Made _ work in other fonts andru -% Wed Oct 12 17:39:49 EDT 1994 Made activate/deactivate work andru -% Wed Feb 08 15:00:31 EST 1995 Made * work again andru -% Wed Jun 7 18:08:23 EDT 1995 Got rid of * andru -% Sun Aug 4 15:58:16 EDT 2002 Rewrite using environments Robert Grimm -% Thu Aug 15 11:39:12 EDT 2002 More documentation andru -% Mon Sep 26 08:14:21 EDT 2016 \protect quotes in captions andru -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Options -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\DeclareOption{sfcode}{\def\ttquot@ttfont{\sf}} -\DeclareOption{small}{\def\ttquot@ttsize{\ifmmode\else\small\fi}} -\DeclareOption{stdbraces}{\def\ttquot@braces{}} -\DeclareOption{bfemph}{\def\ttquot@emfont{\bf}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Save original definitions -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\let\ttquot@mark="% Catch original definition of quotation mark -\let\ttquot@us=_% Catch original definition of underscore - -\def\ttquot@tt@us{\char95} % how to render underscore in tt mode. - -% Change character codes to make them active temporarily. -\catcode`\"=\active% -\catcode`\_=\active% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Change " to place its contents inside {\ttquot@ttfont ... } -% Also, underscores are underscores, not subscripts -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newenvironment{ttquot@ttmode}{% -\mbox\bgroup% -\ttquot@setup% -\def_{\ifmmode\ttquot@us\else\ttquot@tt@us\fi}% -\def"{\protect\end{ttquot@ttmode}}% -}% -{\egroup} - -\def\ttquot@setup{\ttquot@ttfont\ttquot@ttsize\ttquot@braces} - -\def\ttquot@ttfont{\ttfamily} -\def\ttquot@braces{\def\{{\char123}\def\}{\char125}} -\def\ttquot@ttsize{} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Change _ to place its contents inside {\ttquot@emfont ... } -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newenvironment{ttquot@emmode}{% -\ttquot@emfont% -\def_{\protect\end{ttquot@emmode}}% -}% -{} - -\gdef\ttquot@emfont{\em} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Change LaTeX's verbatim mode to use \ttquot@ttfont -% instead of \tt; also, do right thing with _ -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\def\@verbatim{\trivlist \item[]\if@minipage\else\vskip\parskip\fi -\leftskip\@totalleftmargin\rightskip\z@ -\parindent\z@\parfillskip\@flushglue\parskip\z@ -\@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par} -\obeylines \ttquot@ttfont -\@noligs \let\do\@makeother \dospecials -\catcode`\_=13% -\def_{\_}% -\catcode``=13% -} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Macros to turn the package on and off -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\gdef\ttquot@activate{% -\catcode`\"=\active% -\catcode`\_=\active% -\def"{\protect\begin{ttquot@ttmode}}% -\def_{\ifmmode\ttquot@us\else\protect\begin{ttquot@emmode}\fi}% -} - -\gdef\ttquot@deactivate{% -\def"{\ttquot@mark}% -\def_{\ttquot@us}% -\catcode`\"=12% -\catcode`\_=8% -} - -% Restore character codes to avoid messing up other packages. -% Character codes will be turned back on at beginning of document. -\catcode`\"=12 -\catcode`\_=8 - -\let\ttquot@old@citex\@citex - -\def\@citex[#1]#2{ - \edef\ttquot@us@catcode{\the\catcode`\_}% - \catcode`\_=13% - \ttquot@old@citex[#1]#2 - \catcode`\_=\ttquot@us@catcode\relax} - -\let\ttquot@old@bibliography\bibliography - -\def\bibliography#1{% - \catcode`\_=8 - \ttquot@old@bibliography{#1}} - -\ProcessOptions -\AtBeginDocument{\ttquot@activate} diff --git a/semantics/ttquot.sty b/semantics/ttquot.sty deleted file mode 100644 index a740e20b..00000000 --- a/semantics/ttquot.sty +++ /dev/null @@ -1,180 +0,0 @@ -\NeedsTeXFormat{LaTeX2e}[2.09] -\ProvidesPackage{ttquot} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% ttquot.sty -% -% Simple markdown support for LaTeX. (It was developed in 1992 before -% "markdown" existed!) -% -% One of the most common problems is switching conveniently into the -% typewriter font and back. This style file makes the ordinary double -% quotation mark (") serve this function. Note that the meaning of \tt -% may be different in math and text mode, for example if the "times" -% package is being used. -% -% This package also makes underscore characters (_) switch into -% emphasized mode and back, unless inside " quotes or in math mode. This -% makes ordinary variable names easier to type in typewriter font, and -% makes emphasized mode obey a common ASCII text convention. -% -% Options: -% sfcode -% Makes text inside quotation marks come out in \sf font. -% small -% Makes text inside quotation marks come out \small (except in math -% mode.) This is especially useful when using the times package, because -% the Courier and Helvetica fonts are larger than Times. -% stdbraces -% By default, the commands \{ and \} emit ordinary characters 123 and -% 125 inside quotation marks. This works well if you are in \tt font, -% but not so well in a font (e.g., \sf) lacking these characters. Use -% stdbraces to defeat it. -% bfemph -% Make underscore turn on boldface instead of italics. -% -% The following macros are defined and may be used or overridden. -% -% \ttquot@activate Turn on ttquot processing. On by default. -% \ttquot@deactivate Turn off ttquot processing. -% \ttquot@ttmode The 'code' environment introduced by " -% \ttquot@emmode The 'emphasized' environment introduced by _ -% \ttquot@setup Commands that are emitted in the " environment. -% \ttquot@ttfont The font part of tt@setup, By default, \tt. -% \ttquot@ttsize The font size part of tt@setup, By default, nothing. -% \ttquot@emfont The commands that are emitted in the _ environment. -% By default, \em -% \ttquot@braces Another command emitted in the " environment. -% By default, changes braces to use tt font chars. -% The "stdbraces" option defeats this. -% \ttquot@mark Always represents the plain character (") -% \ttquot@us Represents the original meaning of (_) -% -% This style file is maintained by Andrew Myers (andru@cs.cornell.edu) -% -% Change log: -% Fri Nov 6 14:35:49 EST 1992 Added this documentation andru -% Tue Nov 10 23:05:44 EST 1992 Changed underscore to do \em andru -% Wed Nov 11 17:00:00 EST 1992 Fixed various bugs, added * andru -% Tue Feb 16 23:48:20 EST 1993 Fixed "number" bug, added \* andru -% Tue Mar 23 13:39:39 EST 1993 Got rid of a little cruft andru -% Tue Apr 26 16:07:18 EDT 1994 Made _ work in other fonts andru -% Wed Oct 12 17:39:49 EDT 1994 Made activate/deactivate work andru -% Wed Feb 08 15:00:31 EST 1995 Made * work again andru -% Wed Jun 7 18:08:23 EDT 1995 Got rid of * andru -% Sun Aug 4 15:58:16 EDT 2002 Rewrite using environments Robert Grimm -% Thu Aug 15 11:39:12 EDT 2002 More documentation andru -% Mon Sep 26 08:14:21 EDT 2016 \protect quotes in captions andru -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Options -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\DeclareOption{sfcode}{\def\ttquot@ttfont{\sf}} -\DeclareOption{small}{\def\ttquot@ttsize{\ifmmode\else\small\fi}} -\DeclareOption{stdbraces}{\def\ttquot@braces{}} -\DeclareOption{bfemph}{\def\ttquot@emfont{\bf}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Save original definitions -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\let\ttquot@mark="% Catch original definition of quotation mark -\let\ttquot@us=_% Catch original definition of underscore - -\def\ttquot@tt@us{\char95} % how to render underscore in tt mode. - -% Change character codes to make them active temporarily. -\catcode`\"=\active% -\catcode`\_=\active% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Change " to place its contents inside {\ttquot@ttfont ... } -% Also, underscores are underscores, not subscripts -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newenvironment{ttquot@ttmode}{% -\mbox\bgroup% -\ttquot@setup% -\def_{\ifmmode\ttquot@us\else\ttquot@tt@us\fi}% -\def"{\protect\end{ttquot@ttmode}}% -}% -{\egroup} - -\def\ttquot@setup{\ttquot@ttfont\ttquot@ttsize\ttquot@braces} - -\def\ttquot@ttfont{\ttfamily} -\def\ttquot@braces{\def\{{\char123}\def\}{\char125}} -\def\ttquot@ttsize{} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Change _ to place its contents inside {\ttquot@emfont ... } -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newenvironment{ttquot@emmode}{% -\ttquot@emfont% -\def_{\protect\end{ttquot@emmode}}% -}% -{} - -\gdef\ttquot@emfont{\em} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Change LaTeX's verbatim mode to use \ttquot@ttfont -% instead of \tt; also, do right thing with _ -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\def\@verbatim{\trivlist \item[]\if@minipage\else\vskip\parskip\fi -\leftskip\@totalleftmargin\rightskip\z@ -\parindent\z@\parfillskip\@flushglue\parskip\z@ -\@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par} -\obeylines \ttquot@ttfont -\@noligs \let\do\@makeother \dospecials -\catcode`\_=13% -\def_{\_}% -\catcode``=13% -} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% -% Macros to turn the package on and off -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\gdef\ttquot@activate{% -\catcode`\"=\active% -\catcode`\_=\active% -\def"{\protect\begin{ttquot@ttmode}}% -\def_{\ifmmode\ttquot@us\else\protect\begin{ttquot@emmode}\fi}% -} - -\gdef\ttquot@deactivate{% -\def"{\ttquot@mark}% -\def_{\ttquot@us}% -\catcode`\"=12% -\catcode`\_=8% -} - -% Restore character codes to avoid messing up other packages. -% Character codes will be turned back on at beginning of document. -\catcode`\"=12 -\catcode`\_=8 - -\let\ttquot@old@citex\@citex - -\def\@citex[#1]#2{ - \edef\ttquot@us@catcode{\the\catcode`\_}% - \catcode`\_=13% - \ttquot@old@citex[#1]#2 - \catcode`\_=\ttquot@us@catcode\relax} - -\let\ttquot@old@bibliography\bibliography - -\def\bibliography#1{% - \catcode`\_=8 - \ttquot@old@bibliography{#1}} - -\ProcessOptions -\AtBeginDocument{\ttquot@activate} diff --git a/src/main/scala/pipedsl/common/CommandLineParser.scala b/src/main/scala/pipedsl/common/CommandLineParser.scala index 056372a4..58228672 100644 --- a/src/main/scala/pipedsl/common/CommandLineParser.scala +++ b/src/main/scala/pipedsl/common/CommandLineParser.scala @@ -39,13 +39,13 @@ object CommandLineParser { .text("Add debug commands to the generated circuit"), arg[File]("...") .action((x, c) => c.copy(file = x)) - .text("pdsl files to parse"), + .text("pdl files to parse"), cmd("parse") - .text("parses the provided pdsl file and prints to the out file\n") + .text("parses the provided pdl file and prints to the out file\n") .action((_, c) => c.copy(mode = "parse")), cmd("interpret") .action((_, c) => c.copy(mode = "interpret")) - .text("interprets the provided pdsl file and prints the resulting memory state to the out file\n") + .text("interprets the provided pdl file and prints the resulting memory state to the out file\n") .children( opt[Int]("maxIterations") .action((x,c) => c.copy(maxIterations = x)) @@ -59,7 +59,7 @@ object CommandLineParser { .text("provided memory inputs") ), cmd("gen") - .text("generates code for the provided pdsl file and writes the generated bluespec in the 'out' directory\n") + .text("generates code for the provided pdl file and writes the generated bluespec in the 'out' directory\n") .action((_, c) => c.copy(mode = "gen")) .children( opt[String]("addrLockModule")