#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 and TGraph) 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.
• 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:

1. A. Lisitsa and A. Nemytykh. Verification as a parameterized testing (experiments with the SCP4 supercompiler). Programming and Computer Software. vol. 33. 2007
2. 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.
3. 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.
4. SCP 4 : Verification of Protocols
5. 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 mrsc
> set javaOptions += "-Dmrsc.verbose=true"
> test-only mrsc.pfp.test.TicksEvaluationSuite