# KRAM: The Concurrent Rewrite Abstract Machine

From FSL

## ICGT '12

**A Truly Concurrent Semantics for the K Framework Based on Graph Transformations**- Traian Florin Serbanuta and Grigore Rosu
, LNCS 7562, pp 294-310. 2012**ICGT'12**

*Abstract.*This paper gives a truly concurrent semantics with sharing of resources for the K semantic framework, an executable (term-)rewriting-based formalism for defining programming languages and calculi. Akin to graph rewriting rules, the K (rewrite) rules explicitly state what can be concurrently shared with other rules. The desired true concurrency is obtained by translating the K rules into a novel instance of term-graph rewriting with explicit sharing, and then using classical concurrency from the double-pushout (DPO) approach to graph rewriting. The resulting parallel term-rewriting relation is proved sound, complete, and serializable with respect to the jungle rewriting flavor of term-graph rewriting, and, therefore, also to term rewriting.

## Technical Report

**KRAM—Extended Report**- Traian Florin Serbanuta and Grigore Rosu
http://hdl.handle.net/2142/17337, September 2010**Technical Report**

*Abstract.*Term rewriting proved to be a simple, uniform and powerful computational paradigm. Rewrite rules independently match and apply anywhere, unconstrained by the context. Rewriting is particularly appealing for defining truly concurrent systems, since rewrite rules can apply in parallel. Unfortunately, there is an inherent impediment in using term rewriting for defining concurrent systems or programming languages: overlapping rewrite rules*cannot*proceed concurrently. This limitation enforces an interleaving semantics in situations where one may not want it. For example, two threads accessing different regions of memory need to interleave since the corresponding rewrite rules overlap on the memory subterm. Or two message receiving operations of two distributed agents need to interleave since the corresponding rewrite rules overlap on the message pool subterm.

This paper presents the concurrent rewrite abstract machine (KRAM), a generalization of term rewriting in which rules explicitly state what can be concurrently shared with other rules, like in graph rewriting. A parallel rewrite relation is defined and proved sound, complete and serializable with respect to conventional rewriting. The KRAM serves as the computational infrastructure of K, an executable semantic framework in which programming languages, calculi, as well as type systems or formal analysis tools can be defined, making use of configurations, computations and rules. A series of examples are discussed, including a non-trivial higher-order multi-threaded distributed language; all examples were defined and executed using the K-Maude tool.