WWW.DISSERTATION.XLIBX.INFO
FREE ELECTRONIC LIBRARY - Dissertations, online materials
 
<< HOME
CONTACTS



Pages:     | 1 || 3 | 4 |   ...   | 22 |

«Oracle Semantics Aquinas Hobor A Dissertation Presented to the Faculty of Princeton University in Candidacy for the Degree of Doctor of Philosophy ...»

-- [ Page 2 ] --

The advantage of using a computer to check that a property has been demonstrated is that computers are very good at handling the bulk of detail associated with real code, so that one can apply formal techniques to the actual program and still be confident about the result. The disadvantage of automated techniques is that the parts that require human input can be very laborious. Indeed, the endeavor becomes similar to building a large software project, and quite unsuprisingly “proof engineering” becomes very important. For example, good machine-checked proofs, like good software, should be modular so that parts can be re-used in other systems.

1.2.2 Source vs. Target One major problem for formal methods is that the analysis tends to be done on source code, whereas the code that actually runs on the chip is machine code. In between sits the compiler, a very large software engineering artifiact. Any bug in the compiler could cause the machine code to behave in a different way from the source code, invalidating any property guaranteed. Since compilers can easily be hundreds of thousands of lines long, most have many bugs, even when they have been extensively tested.

–  –  –

no-one knew how to handle it satisfactorially. One technique that works in limited cases is to analyze the machine code directly. The problem has been that most real systems are not developed in assembly language, making those techniques useful only in rare circumstances. However, in recent years people have been improving compiler technology, for example with Proof-Carrying Code (PCC), developed in [Nec97], in the hope of addressing this issue.

1.2.3 Certified Compilers, CompCert, and

–  –  –

Most proof-carrying code systems do not guarantee the correct behavior of the compiled code, but instead guarantee that certain incorrect behaviors can never occur. That is, they produced a safety guarantee, not a correctness guarantee. However, in order to soundly apply more general kinds of reasoning at the source level to code at the machine level, a correctness guarantee—that is, a guarantee that source code was correctly translated into machine code by the compiler—was required.

Compilers with this guarantee are called certified. With certified compilers it becomes feasible to connect correctness proofs at the source language to guarantees about how the hardware will actually behave when running the compiled code.

One of the first certified optimizing compilers from a realistic source language to a realistic assembly language was the CompCert compiler, developed by Leroy in [Ler06], which translates a language called C

CHAPTER 1. INTRODUCTION

 minor to the Power PC. CompCert has a correctness proof, machinechecked in Coq, that proves that the compiler translates programs correctly.

Leroy found that using operational semantics was the most convienent for proving his compiler correct. However, when verifying a concrete program, it is frequently more convienent to use an axiomatic semantics, such as Hoare logic [Hoa69]. Separation logic is a variant of Hoare logic that includes elegant rules for reasoning about pointers [Rey02]. Since the focus of this thesis is on concurrency, we will refer to a separation logic for a sequential language as seqential separation logic (SSL).

Appel and Blazy developed a version of SSL for C minor, and constructed a machine-checked soundness proof for it in Coq [AB07]. A soundness proof for an axiomatic semantics demonstrates the connection between that axiomatic semantics and the underlying operational semantics. In other words, if one has a program verified with SSL to have certain properties, the soundness proof demonstates that the program actually has those properties. Depending on the complexities of the desired axiomatic semantics, and the underlying operational semantics, it can be quite difficult to establish soundness.

The result is an end-to-end system: one can take a source program,

–  –  –

shortcoming has been the lack of support for concurrency—all certied compilers in existence have focused on purely sequential settings [LPP05, Ler06, Moo89].

1.2.4 Formal Methods for Concurrency As previously discussed, verification even in a purely sequential setting is difficult enough; adding in concurrent language features usually requires significantly more effort on the part of the verifier. Classic techniques have required verifiers to reason about the state of all the other threads at each program point, which can easily require an exponentially-sized proof.

The proof becomes unmanageably large beacause in a concurrent program different sections of the code interact (typically via shared memory and synchronization operations) despite the lack of explicit connectives such as function calls. This kind of global, whole-program behavior has made it very difficult to reason locally or to use simpler, sequential-style techniques. This is particularly frusterating, since real concurrent systems tend to have large portions of purely sequential code, where the interleaving should not have any important effect on the result. Those sequential portions are often difficult to reason about on their own, and it is painful to be forced to reason simultaneously about some complex sequential feature such as function call and some concurrent feature such as context switching.





–  –  –

tial system, comprising both implementation (code) and verification (proof), and the desire is to add concurrency to that system. However, not only does one have to modify the code to take advantage of concurrency, but also one must modify the proofs, even for those parts of the code that are unchanged and that “should” not be interacting with the concurrency additions.

1.2.5 Concurrent Separation Logic Recently, O’Hearn developed Concurrent Separation Logic (CSL), a Hoare-style logic designed to verify concurrent programs [O’H07]. CSL has two major properties that help solve many of the problems typically associated with the verification of concurrent programs. First, it modularly isolates the different threads of execution from each other, so that when when reasoning about a given thread, one does not have to consider the states of all the other threads, i.e., one can use threadlocal reasoning. Second, the rules of CSL are a proper superset of the rules of SSL. Thus if one has laboriously verified a program with SSL and wishes to add concurrency, all of the parts of the code that have not changed will have exactly the same verification.

As groundbreaking as CSL was, as originally proposed it had several drawbacks. First, some of the language features supported were nonstandard, e.g., for example the treatment of shared local variables.

Second, and more worryingly, O’Hearn did not have a soundness proof.

The lack of standard language features prevents programming with

1.3. THE GOAL OF ORACLE SEMANTICS  standard alogrithms or techniques. Some of these ommissions, such as the lack of functions, were done simply to make an attempt at a soundness proof simpler (that is, functions were not considered to be part of the “core” of the problem1 ). Other features, such as allowing for the dynamic creation and destruction of locks, were missing because it was quite unclear how to prove them sound.

Even with significant simplifications, it was quite difficult to prove CSL sound. Due to the complex nature of concurrency and to a number of subtle issues involving resource invariants, the soundness of CSL was doubted for some time until Brookes developed a soundness proof for it [Bro07]2.

1.3 The Goal of Oracle Semantics The goal of this thesis is to support the verification of concurrent programs in a way that is natural to the end-user and allows for substantial re-use of existing sequential code and associated machine-checked proofs; using this semantics we prove the soundness in Coq of a new concurrent separation logic with first-class locks and threads. The key technical advance is to isolate proofs about sequential language features and proofs about concurrent language features from each other. This In the case of first-order functions, it is true that they are noncore; first-class functions, however, are another story.

“At that time I had no model and was scared about soundness. Then John Reynolds showed surprising subtleties regarding soundness, and we were facing an extremely difficult problem in the semantics of concurrency. We needed expert help, and it arrived in Steve Brookes who rode in and saved the day (and the whole approach).” [O’H]

CHAPTER 1. INTRODUCTION

 substantially simplifies the reasoning for each part, since when reasoning about complex sequential features one does not have to worry about the issues typically associated with concurrency, and when reasoning about complex concurrent features one does not have to worry about all of the messy details involved in pure sequential control flow. This isolation also makes the resulting system more robust, since changes to one part of the system do not require changes in the other.

The key technical advances are

1. A powerful new concurrent language, Concurrent C minor, which is related to to a certified compiler.

2. A new Concurrent Separation Logic with first-class locks and functions.

3. A series of modules and other engineering developments to add concurrency to a certified compiler.

4. A new modal substructural logic, used for the assertions of CSL.

5. A novel concurrent operational semantics that uses the logic in its operational semantics to guarantee lock invariants are obeyed.

6. A new pseudosequential oracle semantics that gives a sequential view of concurrent computation.

–  –  –

8. A soundness proof of CSL with respect to the concurrent operational semantics.

Note about proofs and Coq. This thesis is about two related but distinct developments. First, it is about a series of mathematical ideas developed to prove a soundness result. Second, it is about the engineering work required to make a 60,000 line soundness proof check in the Coq theorem prover. From time to time, the two developments have influenced each other, sometimes leading to new mathematics or better engineering. When the presentation here diverges from the Coq development there are two likely causes. First, in general our mathematical understanding is ahead of our Coq implementation; therefore, from time to time in the text we present a cleaner or more elegant definition than the one in the Coq proof. Second, we frequently simplify some of the significant complexities from the Coq definitions so that the kernel of the mathematical idea is clear. When we diverge from the Coq implementation we try to mention this fact in the text.

1.4 Structure of Thesis First, since the verification of concurrent programs is a fairly extensive goal, a major part of the research is learning about existing systems that support parts of that goal, so that they can be connected together.

Since the ideal end-goal is to have guarantees about the machine code that actually executes, we develop our system in Coq for the C minor

CHAPTER 1. INTRODUCTION

 language, to enable a connection to Leroy’s CompCert certified compiler. This and other related work is introduced in chapter 2.

Second, since C minor is a sequential language, we add concurrent statements to create the new language Concurrent C minor. We add the standard concurrency primitives lock and unlock, and we allow the kind of dynamic lock creation and destruction that programmers are used to. We also add a fork statement to start a new thread of execution. Together, these statements allow for a familiar, well-understood concurrency setting in the style of Pthreads. The full details of Concurrent C minor language are discussed in chapter 3.

Third, we extend and modify O’Hearn’s CSL to reason about our new language. First-class locks and functions (that is, locks that can guard function pointers and function pointers that can take locks as arguments) turn out to be a significant technical advance, and were one of the substantial challanges in building the model. Our new CSL is similar to the one independently developed by Gotsman et al, indicating that it is the natural way to extend CSL to handle Pthreads-style concurrency. Our version of CSL is developed in chapter 4.

Fourth, we define a simple concurrent operational semantics for Concurrent C minor called the erased concurrent operational semantics to demonstrate that we have a realistic operational semantics for concurrency. The erased concurrent operational semantics is presented in chapter 5.

–  –  –

quential and concurrent features of the language from each other. The modularization also isolates the concurrency system from being dependent on the C minor language, which will be helpful when extending the CompCert compiler. The modularization is explained in chapter 6.

Sixth, to develop the semantic model for invariants, we develop a modal logic. This logic allows us to reason elegantly about different requirements in an orthogonal, modular fashion, allowing us to build up our different invariants cleanly. Our modal logic is quite powerful, allowing for contravariant recursion, impredicative quantification over both values and predicates, function pointers, and other features required for handling programs with abstraction. After we model our invariants using our modal logic, we must next develop a model for our modal logic, which we do in the style of Appel, Mellies, Richards, and Vouillon [AMRV07]. Our modal logic and the associated semantic model is presented in chapter 7.

Seventh, we define a more complex concurrent operational semantics called the unerased concurrent operational semantics. The new semantics does substantial additional bookkeeping that guarantees that it gets stuck on ill-synchronized programs; if we can show that a program does not get stuck, then we know that it is well-synchronized. We prove an erasure theorem that guarantees that if the unerased machine is not stuck then the erased machine is not stuck. The unerased concurrent operational semantics of Concurrent C minor is presented in chapter 8.



Pages:     | 1 || 3 | 4 |   ...   | 22 |


Similar works:

«THE EFFECTS OF ELEMENTARY DEPARTMENTALIZATION ON MATHEMATICS PROFICIENCY Nicole C. Taylor-Buckner Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy under the Executive Committee of the Graduate School of Arts and Sciences COLUMBIA UNIVERSITY © 2014 Nicole C. Taylor-Buckner All rights reserved ABSTRACT THE EFFECTS OF ELEMENTARY DEPARTMENTALIZATION ON MATHEMATICS PROFICIENCY Nicole C. Taylor-Buckner Mathematics education in the elementary schools has...»

«Department of Educational Administration Doctoral Degree K-12 Educational Administration Student / Faculty Handbook For accepted / enrolled students Last Updated: 08/20/2015 TABLE OF CONTENTS I. Program Overview • PhD Program Mission and Philosophy • PhD Program Expectations II. Program Components Credit Accrual Preliminary • Exam Comprehensive • Exam Research Practicum • Dissertation Proposal • Dissertation Defense • III. Degree Requirements Residency Requirement • Time...»

«FEMALE DISCOURSES: POWERFUL AND POWERLESS SPEECH IN SIR THOMAS MALORY’S LE MORTE DARTHUR By YEKATERINA ZIMMERMAN A DISSERTATION PRESENTED TO THE GRADUATE SCHOOL OF THE UNIVERSITY OF FLORIDA IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY UNIVERSITY OF FLORIDA Copyright 2005 by Yekaterina Zimmerman ACKNOWLEDGMENTS I would like to thank the chair of my committee, Dr. Diana Boxer, for being my mentor for all these years, for her guidance, emotional support and...»

«CARDIOVASCULAR ENDOTHELIAL REGENERATION ON AN ELECTROSPUN SCAFFOLD by XING ZHANG YOGESH K. VOHRA, COMMITTEE CHAIR SUSAN L. BELLIS DERRICK R. DEAN ALAN W. EBERHARDT VINOY THOMAS A DISSERTATION Submitted to the graduate faculty of the University of Alabama at Birmingham, in partial fulfillment of the requirement for the degree of Doctor of Philosophy BIRMINGHAM, ALABAMA 2010   CARDIOVASCULAR ENDOTHELIAL REGENERATION ON AN ELECTROSPUN SCAFFOLD XING ZHANG DOCTOR OF PHILOSOPHY IN BIOMEDICAL...»

«Gepubliceerd op Esthetica (http://www.estheticatijdschrift.nl) Wittgenstein and the Visual Experience of Depiction Jonathan Friday Ludwig Wittgenstein’s discussion of aspect perception in the latter part of the Philosophical Investigations is generally credited with inspiring an important strand in contemporary explanations of depiction in which the visual experience of perceivers of pictures has a key role in the explanation. Although theorists working in this tradition have modified his...»

«INTEGRATING SEQUENCE STRATIGRAPHY AND ROCKPHYSICS TO INTERPRET SEISMIC AMPLITUDES AND PREDICT RESERVOIR QUALITY A DISSERTATION SUBMITTED TO THE DEPARTMENT OF GEOPHYSICS AND THE COMMITTEE ON GRADUATE STUDIES OF STANFORD UNIVERSITY IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY Tanima Dutta August 2009 © Copyright by Tanima Dutta 2009 All Rights Reserved ii I certify that I have read this dissertation and that, in my opinion, it is fully adequate in scope and...»

«INSTITUTION BUILDING IN AN EMERGING INDUSTRY: LESSONS FROM THE CARBON OFFSET INDUSTRY A DISSERTATION SUBMITTED TO THE FACULTY OF THE GRADUATE SCHOOL OF THE UNIVERSITY OF MINNESOTA BY HANS NIKOLAS RAWHOUSER IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY ALFRED MARCUS, ADVISER MAY 2012 © Hans Rawhouser 2012 Acknowledgements When I entered the PhD program I did not fully comprehend the many real risks involved and my degree of dependence on so many others to...»

«The
Elusive
Made
Present:
 Art
and
the
Incipiency
of
Images
 Troy Rhoades A Thesis In The Humanities Program Presented in Partial Fulfillment of the Requirements For the Degree of Doctor of Philosophy at Concordia University Montreal, Quebec, Canada June, 2011 © Troy Rhoades 2011 CONCORDIA UNIVERSITY SCHOOL OF GRADUATE STUDIES This is to certify that the thesis prepared By: Troy Rhoades Entitled: The Elusive Made Present: Art and Incipiency of Images and submitted in...»

«HOW METHODISTS WERE MADE: THE ARMINIAN MAGAZINE AND SPIRITUAL TRANSFORMATION IN THE TRANSATLANTIC WORLD, 1778-1803 by LIAM IWIG-O’BYRNE Presented to the Faculty of the Graduate School of The University of Texas at Arlington in Partial Fulfillment of the Requirements for the Degree of DOCTOR OF PHILOSOPHY THE UNIVERSITY OF TEXAS AT ARLINGTON May 2008 Copyright © by Liam Iwig-O’Byrne 2008 All Rights Reserved ACKNOWLEDGEMENTS I would like to thank my committee for their work on my behalf,...»

«Soldiering in the Canadian Forces: How and Why Gender Counts! Lynne Gouliquer Department of Sociology McGill University, Montreal A thesis submitted to McGill University in partial fulfilment of the requirements of the degree of Doctor of Philosophy © Lynne Gouliquer, 2011 Table of Contents List of Tables Abstract Sommaire Acknowledgements Chapter 1 Introduction Historical  Synopsis Thesis  Overview Chapter 2 Theorizing Gender and Organisations Analysing  Gender  Inequalities  at...»

«Course Handbook BA (Hons) Professional Cookery with foundation London College of Hospitality & Tourism BA (Hons) Food and Professional Cookery with foundation Course Handbook 2016-2017 Section BA (Hons) Food and Professional Cookery with foundation Course Handbook Contents Page No. Section 1 Key Information 1.1 Welcome to the Course 4 1.2 Overview of the Course 5 1.3 Sources of Help and Support 6 1.4 Facts and Figures 8 1.5 Your Responsibilities 9 Section 2 Structure and Content 2.1...»

«Colón 1   Mysterious Melodies: Futurism, Primitivism, and the Onomatopoetics of ultraísmo and negrismo David Colón Texas Christian University In his influential essay “Posibilidades creacionistas,” published in Cervantes in October of 1919, Gerardo Diego schematizes the literary concept of the imagen, the most vital compositional facet of the Spanish and Latin American poetic avant-gardes of the 1920s. Diego begins by identifying the various forms of the imagen, rhetorically explained...»





 
<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.