KRAM: The Concurrent Rewrite Abstract Machine

From FSL
Jump to: navigation, search

ICGT '12

A Truly Concurrent Semantics for the K Framework Based on Graph Transformations
Traian Florin Serbanuta and Grigore Rosu
ICGT'12, LNCS 7562, pp 294-310. 2012
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.
PDF, Slides(PDF), K, DOI, ICGT'12, BIB

Technical Report

KRAM—Extended Report
Traian Florin Serbanuta and Grigore Rosu
Technical Report, September 2010
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.

Personal tools