Files in this item

FilesDescriptionFormat

application/pdf

application/pdfSerbanuta_Traian.pdf (4MB)
(no description provided)PDF

Description

Title:A rewriting approach to concurrent programming language design and semantics
Author(s):Serbanuta, Traian Florin
Director of Research:Rosu, Grigore
Doctoral Committee Chair(s):Rosu, Grigore
Doctoral Committee Member(s):Ball, Thomas; Marinov, Darko; Meseguer, José; Parthasarathy, Madhusudan
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Degree:Ph.D.
Genre:Dissertation
Subject(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.
Issue Date:2011-01-14
URI:http://hdl.handle.net/2142/18252
Rights Information:Copyright 2010 Traian F. Serbanuta
Date Available in IDEALS:2011-01-14
Date Deposited:December 2


This item appears in the following Collection(s)

Item Statistics