Withdraw
Loading…
A rewriting approach to concurrent programming language design and semantics
Serbanuta, Traian Florin
Loading…
Permalink
https://hdl.handle.net/2142/18252
Description
- Title
- A rewriting approach to concurrent programming language design and semantics
- Author(s)
- Serbanuta, Traian Florin
- Issue Date
- 2011-01-14T22:41:18Z
- Director of Research (if dissertation) or Advisor (if thesis)
- Rosu, Grigore
- Doctoral Committee Chair(s)
- Rosu, Grigore
- Committee Member(s)
- Ball, Thomas
- Marinov, Darko
- Meseguer, José
- Parthasarathy, Madhusudan
- Department of Study
- Computer Science
- Discipline
- Computer Science
- Degree Granting Institution
- University of Illinois at Urbana-Champaign
- Degree Name
- Ph.D.
- Degree Level
- Dissertation
- Keyword(s)
- programming languages design
- rewriting
- concurrency
- rewriting logic
- runtime verification
- memory safety
- Abstract
- A plethora of programming languages have been and continue to be developed to keep pace with hardware advancements and the ever more demanding requirements of software development. As these increasingly sophisticated languages need to be well understood by both programmers and implementors, precise specifications are increasingly required. Moreover, the safety and adequacy with respect to requirements of programs written in these languages needs to be tested, analyzed, and, if possible, proved. This dissertation proposes a rigorous approach to define programming languages based on rewriting, which allows to easily design and test language extensions, and to specify and analyze safety and adequacy of program executions. To this aim, this dissertation describes the K framework, an executable semantic framework inspired from rewriting logic but specialized and optimized for programming languages. The K framework consists of three components: (1) a language definitional technique; (2) a specialized notation; and (3) a resource-sharing concurrent rewriting semantics. The language definitional technique is a rewriting technique built upon the lessons learned from capturing and studying existing operational semantics frameworks within rewriting logic, and upon attempts to combine their strengths while avoiding their limitations. The specialized notation makes the technical details of the technique transparent to the language designer, and enhances modularity, by allowing the designer to specify the minimal context needed for a semantic rule. Finally, the resource-sharing concurrent semantics relies on the particular form of the semantic rules to enhance concurrency, by allowing overlapping rule instances (e.g., two threads writing in different locations in the store, which overlap on the store entity) to apply concurrently as long as they only overlap on the parts they do not change. The main contributions of the dissertation are: (1) a uniform recasting of the major existing operational semantics techniques within rewriting logic; (2) an overview description of the K framework and how it can be used to define, extend and analyze programming languages; (3) a semantics for K concurrent rewriting obtained through an embedding in graph rewriting; and (4) a description of the K-Maude tool, a tool for defining programming languages using the K technique on top of the Maude rewriting language.
- Graduation Semester
- 2010-12
- Permalink
- http://hdl.handle.net/2142/18252
- Copyright and License Information
- Copyright 2010 Traian F. Serbanuta
Owning Collections
Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at IllinoisDissertations and Theses - Computer Science
Dissertations and Theses from the Dept. of Computer ScienceManage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…