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 MRSCPfp
> set javaOptions += "-Dmrsc.verbose=true"
> testOnly mrsc.pfp.test.TicksEvaluationSuite