Technical Reports on K

From FSL
Jump to: navigation, search


Note to readers: The material presented in these reports serves as a basis for programming language design and semantics classes and for several research projects. The most recent of the reports aims at giving a global snapshot of the current status of the K framework. Consequently, this work will be published on a version by version basis, each including and improving (parts of) the previous ones, probably over a period of several years. My plan is to eventually transform this material into a book, so your suggestions and criticisms are welcome.


(December 2007)
K: A Rewriting-Based Framework for Computations — Preliminary version —

Grigore Rosu
Technical report UIUCDCS-R-2007-2926 and UILU-ENG-2007-1827, December 2007
Abstract. K is a definitional framework based on term rewriting, in which programming languages, calculi, as well as type systems or formal analysis tools can be defined making use of special list and/or set structures, called cells, which can be potentially nested. In addition to cells, K definitions contain equations capturing structural equivalences that do not count as computational steps, and rewrite rules capturing computational steps or irreversible transitions. Rewrite rules in K are unconditional, i.e., they need no computational premises (they are rule schemata and may have ordinary side conditions, though), and they are context-insensitive, so in K rewrite rules apply concurrently as soon as they match, without any contextual delay or restrictions.

The distinctive feature of K compared to other term rewriting approaches in general and to rewriting logic in particular, is that K allows rewrite rules to apply concurrently even in cases when they overlap, provided that they do not change the overlapped portion of the term. This allows for truly concurrent semantics to programming languages and calculi. For example, two threads that read the same location of memory can do that concurrently, even though the corresponding rules overlap on the store location being read. The distinctive feature of K compared to other frameworks for true concurrency, like chemical abstract machines (Chams) or membrane systems (P-systems), is that equations and rewrite rules can match across multiple cells and thus perform changes many places at the same time, in one step.

K provides special support for list cells that carry computational meaning, called computations. Computations are special \curvearrowright-separated lists T_1 \curvearrowright T_2 \curvearrowright \dots \curvearrowright T_n comprising computational tasks, thought of as having to be processed sequentially. Computation (structural) equations or heating/cooling equations, which technically are ordinary equations but which practically tend to have a special computational intuition (reason for which we use the equality symbol \rightleftharpoons instead of = for them), allow to regard computations (finitely) many different, but completely equivalent ways. For example, in a language with an addition operation whose arguments can be evaluated in non-deterministic order, a computation a_1 + a_2 may also be regarded as a_1 \curvearrowright \square + a_2, with the intuition schedule a_1 for processing and freeze a_2 in freezer \square + \_, but also as a_2 \curvearrowright a_1 + \square. Computations can be handled like any other terms in a rewriting environment, that is, they can be matched, moved from one place to another in the original term, modified, or even deleted. A term may contain an arbitrary number of computations, so K can be naturally used to define concurrent languages or calculi. Structural equations can rearrange computations, so that rewrite rules can match and apply. Equations and rules can apply anywhere, in particular in the middle of computations, not only at their top. However, rules corresponding to inherently sequential operations (such as reads/writes of variables in the same thread) must be designed with care, to ensure that they are applied only at the top of computations.

K achieves, in one uniform framework, the benefits of both Chams and reduction semantics with evaluation contexts (context reduction), at the same time avoiding what may be called the rigidity to chemistry of the former and the rigidity to syntax of the latter. Any Cham and any context reduction definition can be captured in K with minimal (in our view zero) representational distance. K can support concurrent language definitions with either an interleaving or a true concurrency semantics. K definitions can be efficiently executed on existing rewrite engines, thus providing interpreters for free directly from formal language definitions. Additionally, general-purpose formal analysis techniques and tools developed for rewrite logic, such as state space exploration for safety violations or model-checking, give us corresponding techniques and tools for the defined languages, at no additional development cost.
PDF, ZIP, TR@UIUC, BIB


(December 2006)
K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation Version 2

Grigore Rosu
Technical report UIUCDCS-R-2006-2802, December 2006
Abstract. K is an algebraic framework for defining programming languages. It consists of a technique and of a specialized and highly optimized notation. The K-technique, which can be best explained in terms of rewriting modulo equations or in terms of rewriting logic, is based on a first-order representation of continuations with intensive use of matching modulo associativity, commutativity and identity. The K-notation consists of a series of high-level conventions that make the programming language definitions intuitive, easy to understand, to read and to teach, compact, modular and scalable. One important notational convention is based on context transformers, allowing one to automatically synthesize concrete rewrite rules from more abstract definitions once the concrete structure of the state is provided, by “completing” the contexts in which the rules should apply. The K framework is introduced by defining FUN, a concurrent higher-order programming language with parametric exceptions. A rewrite logic definition of a programming language can be executed on rewrite engines, thus providing an interpreter for the language for free, but also gives an initial model semantics, amenable to formal analysis such as model checking and inductive theorem proving. Rewrite logic definitions in K can lead to automatic, correct-by-construction generation of interpreters, compilers and analysis tools.
PDF, TR@UIUC, BIB


(December 2005)
K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation Version 1

Grigore Rosu
Technical Report UIUCDCS-R-2005-2672, December 2005
Abstract. K is an algebraic framework for defining programming languages. It consists of a technique and of a specialized and highly optimized notation. The K-technique, which can be best explained in terms of rewriting modulo equations or in terms of rewriting logic, is based on a first-order representation of continuations with intensive use of matching modulo associativity, commutativity and identity. The K-notation consists of a series of high-level conventions that make the programming language definitions intuitive, easy to understand, to read and to teach, compact, modular and scalable. One important notational convention is based on context transformers, allowing one to automatically synthesize concrete rewrite rules from more abstract definitions once the concrete structure of the state is provided, by "completing" the contexts in which the rules should apply. The K framework is introduced by defining FUN, a concurrent higher-order programming language with parametric exceptions. A rewrite logic definition of a programming language can be executed on rewrite engines, thus providing an interpreter for the language for free, but also gives an initial model semantics, amenable to formal analysis such as model checking and inductive theorem proving. Rewrite logic definitions in K can lead to automatic, correct-by-construction generation of interpreters, compilers and analysis tools.
PDF, Experiments, BIB


(Fall 2003)
CS322 Lecture notes

Grigore Rosu
Technical Report http://hdl.handle.net/2142/11385, December 2003
Abstract. This report contains the complete lecture notes for CS322, Programming Language Design, taught by Grigore Rosu in the Fall 2003 semester at the University of Illinois at Urbana Champaign. This large PDF document has been generated automatically from the CS322's website at: http://fsl.cs.uiuc.edu/~grosu/classes/2003/fall/cs322/. Of particular importance is the novel technique for defining concurrent languages that starts at page 673, based on a first-order representation of computations (called "continuations" for simplicity there, though only their suffix is an actual "continuation structure").
PDF, Matching Logic, DOI, BIB

Personal tools
Namespaces

Variants
Actions
Navigation