Programming Language Semantics using K — true concurrency through term-graph rewriting —

Developed as a rewriting formalism for describing the operational semantics of programming languages, the K framework proposes a new notation for (term) rewrite rules which identifies a read-only context (or interface) which is not changed by a rewrite rule. This allows for enhancing the transition system to model one-step concurrency with sharing of resources such as concurrent reads of
the same memory location and concurrent writes of distinct memory locations.
Given that graph transformations offer theoretical support for achieving parallel rewriting with sharing of resources, and that the term-graph rewriting approaches were developed as sound and complete means of representing and implementing rewriting, it seems natural to give semantics to K through term-graph rewriting. However, the existing term-graph rewriting approaches aim at efficiency: rewrite common subterms only once, without attempting to use context-sharing information for enhancing the potential for concurrency. Consequently, the concurrency achieved by current termgraph rewriting approaches is no better than that of standard rewriting. Moreover, the efficiency gained by sharing subterms can inhibit behaviors in non-deterministic (e.g., concurrent) systems.

This talk summarizes the efforts of endowing K with a (novel) term-graph rewriting semantics developed with the aim of capturing the intended concurrency the K framework. Challenges encountered during this process and ideas for future development are presented and proposed for discussion.