University of Illinois Urbana-Champaign

KRAM--Extended Report

Șerbănuță, Traian Florin; Rosu, Grigore

Content Files
serbanuta-rosu-2010-tr.pdf

Permalink

https://hdl.handle.net/2142/17337

Description

Title
KRAM--Extended Report
Author(s)
  • Șerbănuță, Traian Florin
  • Rosu, Grigore
Issue Date
2010-09-22
Keyword(s)
  • rewriting
  • graph rewriting
  • rewriting logic
  • rewriting logic semantics
  • concurrency
Date of Ingest
2010-09-22T21:24:01Z
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.
Type of Resource
text
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/17337

Owning Collections

Research and Tech Reports - Computer Science PRIMARY