mrsc

KO | EN

gitlite — search

#javascript #python #hacktoberfest #typescript #llm #machine-learning #rust #linux #macos #windows #awesome #cli #mcp #openai

(★ 33)

A toolkit for building multi-result supercompilers

mrsc Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# 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_. 
<a href="http://pat.keldysh.ru/~ilya/papers/2011-branching-growth.pdf">pdf</a> (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. 
<a href="http://www.keldysh.ru/papers/2011/source/prep2011_77_eng.pdf">pdf</a>

## 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. <a href="http://refal.botik.ru/protocols/">SCP 4 : Verification of Protocols</a>
5. <a href="http://pat.keldysh.ru/jver/">The project JVer</a>

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 <a href="http://isabelle.in.tum.de/">Isabelle</a> 
(`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](https://github.com/ilya-klyuchnikov/mrsc/blob/master/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
```

mrsc

mrsc Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

mrsc

mrsc Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README