A toolkit for building multi-result supercompilers
MRSC is a toolkit for rapid design and prototyping of (multi-result) supercompilers. MRSC 1.0 provides generic data structures and operations for building supercompilers based on the concept of graph of configurations. A supercompiler is encoded as a set of graph rewrite rules.
The theory behind MRSC is described in the following papers:
MRSC is divided in a number of packages:
mrsc.core
SGraph
and TGraph
) for representing a graph of configurations and operationsGraphRewriteRules
for encoding the logic of supercompilation in terms of rewriting rules.GraphGenerator
for incremental producing all possible graphs of configurationsmrsc.counters
The entry point to this example is mrsc/counters/demo.scala
(just launch it to see results in the console).
The package mrsc.counters
contains an example of building a traditional (single-result) supercompiler and a (novel)
multi-result supercompiler for counter systems. This example is inspired by works by Andrei Nemytykh, Alexei Lisitsa
and Andrei Klimov:
The works [1, 2, 4, 5] use the following approach for verification of protocols: express a protocol and its safety
property as a Java of Refal program, supercompile a boolean expression stating the safety property of protocol -
from the structure of supercompiled expression it will follow the safety of protocol. Following [3], we
created a tiny language (of configurations) for encoding states of protocols (mrsc/counters/language.scala
).
Then protocols are expressed in Scala directly - as a DSL over the language of configurations
(mrsc/counters/protocols.scala
). There are two supercompilers in mrsc/counters/rules.scala
encoded as graph
rewrite rules - traditional single-result one and multi-result one. These supercompilers build graphs of
configurations for a given protocol. Using a graph of configurations, we are able to produce a proof
of safety of a protocol for a proof assistant Isabelle
(mrsc/counters/proof.scala
). Demo application in mrsc/counters/demo.scala
puts all things together:
for a number of protocols traditional supercompiler is launched (as in [3]), multi-result supercompiler is launched and
the smallest graphs is then selected from a set of graphs generated by multi-result supercompiler.
The smallest graph is then residuated into a proof for Isabelle. More details are in an upcoming paper.
The output of demo is shown in proofs.md.
By default, tests and samples output is note verbose (to prevent a garbage in output). However, if you really want to see all details:
> project MRSCPfp
> set javaOptions += "-Dmrsc.verbose=true"
> testOnly mrsc.pfp.test.TicksEvaluationSuite