MRSC
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.
Papers
The theory behind MRSC is described in the following papers:
- Ilya Klyuchnikov and Sergei Romanenko. Multi-Result Supercompilation as Branching Growth of the Penultimate Level in Metasystem Transitions. Ershov Informatics Conference 2011. pdf (Revised version is in LNCS 7162, pp. 210–226, 2012)
- Ilya Klyuchnikov and Sergei Romanenko. MRSC: a toolkit for building multi-result supercompilers. Preprint 77. Keldysh Institute of Applied Mathematics, Moscow. 2011. pdf
Code structure
MRSC is divided in a number of packages:
mrsc.core
- Generic data structures (
SGraph
andTGraph
) for representing a graph of configurations and operations on them. - An abstraction
GraphRewriteRules
for encoding the logic of supercompilation in terms of rewriting rules. - The component
GraphGenerator
for incremental producing all possible graphs of configurations for a given set of rewriting rules.
- Generic data structures (
mrsc.counters
- Example of a very simple (but non-trivial!) supercompiler for counter systems (see below).
Example: generating proofs of safety of cache-coherence protocols
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:
- A. Lisitsa and A. Nemytykh. Verification as a parameterized testing (experiments with the SCP4 supercompiler). Programming and Computer Software. vol. 33. 2007
- Andrei V. Klimov, A Java Supercompiler and its Application to Verification of Cache-Coherence Protocols. In: Perspectives of Systems Informatics: 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers. Lecture Notes in Computer Science, volume 5947/2010, pages 185-192. Springer Berlin / Heidelberg, 2010.
- Andrei V. Klimov, Solving Coverability Problem for Monotonic Counter Systems by Supercompilation. In: E.M. Clarke, I. Virbitskaite, A. Voronkov (eds.), Proceedings of the Ershov Informatics Conference (PSI 2011), June 17 – July 01, 2011, Akademgorodok, Novosibirsk, Russia. Novosibirsk: Ershov Institute of Informatics Systems, 2011. P. 92-103.
- SCP 4 : Verification of Protocols
- The project JVer
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.
Tests and examples
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