FREE ELECTRONIC LIBRARY - Dissertations, online materials

Pages:   || 2 | 3 | 4 | 5 |   ...   | 22 |

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

-- [ Page 1 ] --

Oracle Semantics

Aquinas Hobor

A Dissertation

Presented to the Faculty

of Princeton University

in Candidacy for the Degree

of Doctor of Philosophy

Recommended for Acceptance

By the Department of

Computer Science

Advisor: Andrew W. Appel

November 

Copyright c  Aquinas Hobor. All rights reserved.


We define a Concurrent Separation Logic with first-class locks and

threads for the C language, and prove its soundness in Coq with respect to a compilable operataional semantics.

We define the language Concurrent C minor, an extension of the C minor language of Leroy. C minor was designed as the highest-level intermediate language in the CompCert certified ANSI C compiler, and we add to it lock, unlock, and fork statements to make Concurrent C minor, giving it a standard Pthreads style of concurrency. We define a Concurrent Separation Logic for Concurrent C minor, which extends the original Concurrent Separation Logic of O’Hearn to handle firstclass locks and threads.

We then prove the soundness of the logic with respect to the operational semantics of the language. First, we define an erased concurrent operational semantics for Concurrent C minor that is a reasonable abstraction for concurrent execution on a real machine. Second, we define a new modal substructural logic which we use as the model for assertions in Concurrent Separation Logic. Third, we define an unerased iii concurrent operational semantics for Concurrent C minor that keeps track of additional bookkeeping to demonstrate the programs are wellbehaved. Fourth, we define an oracle semantics that is a thread-local semantics of Concurrent C minor; this allows us to separate the metatheory of sequential and concurrent computation from each other. Fifth, we give a new semantics to the Hoare tuple using our modal substructural logic that connects Concurrent Separation Logic to our oracle semantics and then connect our oracle semantics to our concurrent semantics.

Our soundness proofs are largely implemented in 60,000 lines of Coq; our modular proof design allows us to largely reuse a significant portion of the soundness proofs of the sequential subset of Concurrent Separation Logic developed by Appel and Blazy. Our ability to reuse those proofs gives us confidence that we will be able to modify the CompCert compiler proofs to handle Concurrent C minor in the future.

iv Acknowledgements A PhD takes considerable effort, and I am very grateful to the many people who have provided friendship and support during my five years at Princeton. I would like to acknowledge the following people.

My advisor, Andrew Appel, for being extremely generous with his time and energy. I have very much enjoyed learning from and working with him and am very proud of what we have done. It has been fun.

My thesis readers, David Walker and Peter O’Hearn, provided helpful suggestions to improve the text and did a wonderful job reading a long thesis in a short time. I would also like to thank my nonreaders, Brian Kernighan and Vivek Pai, for their support.

My friends near and far, including Ian Adams, Stephen Adams, David Beazley, C.J. Bell, Christian Bienia, Elizabeth Cheehy, Manuvir Das, Rob Dockins, M. and Mme. Dubosc, R.J. Dragani, Gilles Goulas, Carl Haefling and Pam Johnson, Joe Helmer, Mark Kormes, Jason (Wen Di) Li, David MacQueen, Francesco Zappa Nardelli, Travis Pew, Christopher Richards, Ari Schwayder, Tushar and Rupa Shanbhag, Chris Sherman, Colleen Smith, Dan Suberviola, Charlie Trapp, Steve v Wilson, and Daniel Wang.

My in-laws, Steve and Fonde Werts, for being so kind and generous to their son in law. My brother in-law, Charlie Werts, deserves special mention, among other reasons, for his loan of the somewhat incomprehensible yet enjoyable anime series RahXephon. My three grandparentsin-law—Ernie, Joe, and Martha—have been very generous as well.

My family, including my mother, Nancy Hobor; my father, Mike Hobor; my Grandmother, Jane Coulson; and last (but probably not least) my brother, Justinian Hobor. Few things in life give me more pleasure than blowing up his wonders in Civ 4. My Aunt Nancy and Uncle Andy have been very generous in letting me and my wife visit them in Maine, which we have throughly enjoyed. My Aunt Jane and Uncle Jim helped make New Jersey more hospitable. I would also like to thank my cousin George Ellis for letting me stay with him when I visited Rochester.

Finally, my wonderful wife, Lucy Day. We made it!

This research was supported in part by National Science Foundation grant CCF-0540914. In addition, I gratefully acknowledge three summer internships and the people who made them possible: the Program Analysis Group at Microsoft Redmond (Stephen Adams), Lapides Asset Management (Steve Wilson), and the MOSCOVA project at INRIA Rocquencourt (Francesco Zappa Nardelli).

–  –  –

A.4 Private definitions relating public to private.......  A.5 Public interface to acquire resource............ 

–  –  –

2.4 Models of the Sequential Separation Logic Operators.... 

2.5 Continuation-passing style definition of Hoare tuple..... 

2.6 Axiomatic Semantics of Separation Logic (without call and

–  –  –

4.2 Resource invariant for example program........... 

5.1 Erased sequential step relation................. 

5.2 Erased concurrent step relation................ 

–  –  –

6.4 Interface for extensible semantics............... 

6.5 Axioms for Extensible Semantics............... 

6.6 Axioms for C minor memory model.............. 

6.7 Basic definitions for Extensible Semantics.......... 

–  –  –

7.7 Models of substructural assertions............... 

7.8 Rules for reasoning in the modal substructural logic..... 

7.9 Models of Concurrent Separation Logic assertions...... 

7.10 Logical implication in the logic................ 

7.11 Extensionality, validity, precision, and tightness....... 

–  –  –

8.1 Simplified subset of sequential step relation......... 

8.2 The consult relation of the sequential submachine...... 

8.3 Sequential steps in the concurrent step relation....... 

–  –  –

9.1 The oracle allows for reasoning after a concurrent instruction 

9.2 Oracular projection....................... 

9.3 Running the other threads................... 

9.4 The oracular consult relation.................. 

10.1 Oracular safety......................... 

10.2 Na¨ continuation-passing style definition of Hoare tuple..  ıve

10.3 A modal Hoare tuple...................... 

–  –  –


1.1 Concurrency and Multiple Cores Since the 1960s, programmers have utilized concurrency to make their programs faster and to better interact with the external world; however, concurrent programs have been notoriously difficult to develop. In the 1970s, Dijkstra and Hoare proposed constructs such as semaphores to handle the resulting difficulties in [Dij68, Hoa74, Hoa78], but even with them writing concurrent software was extremely time-consuming and error-prone. Therefore people avoided writing concurrent programs as long as computer manufacturers were able to relentlessly crank out chips that could run sequential code faster and faster.

Unfortunately, starting in 2003, manufacturers found it difficult to continue to increase the clock speed, due to factors such as heat retention. To continue to improve the processing power of their chips,

–  –  –

manufacturers began to incorporate multiple CPU cores into a single chip. Simply stated, the idea was that a two-core chip would be able to execute as many instructions as a single-core chip executing at twice the clock speed. Since 2003 it appears to be easier to increase the number of cores than to increase the clock speed, multi-core processors are expected to be pervasive in the future.

However, there are significant problems involved in using a multicore system as opposed to a single-core one. First, even in the best of cases, there is overhead for communication between the multiple cores, so that in fact, even under ideal conditions, a two-core system will perform worse than a single-core system with twice the clock speed.

This problem, while annoying, is not fatal. A more severe problem is that to really take advantage of multiple cores, one must write highly concurrent programs.

Since historically programmers avoided concurrency, when computer manufacturers began to incorporate dual-core processors into their consumer product lines in 2005, the second core was noticably underutilized. Manufacturers’ plans to offer chips with 256 or more cores seemed unjustified, given the low utilization of the multiple cores. For any large number of cores to be useful, programs will have to utilize substantially more concurrency.

–  –  –

program will behave. Moreover, testing is very difficult, since typically concurrency bugs are not reproduceable due to the interaction with the scheduler, which is usually nondeterministic.

The first techniques to handle the difficulties of concurrent programming were various programming disciplines. The earliest of these were monitors, introduced by Hoare [Hoa74] and Hansen [Han93], and semaphores, introduced by Dijkstra [Dij68]. Other common programming disciplines and techniques include condition variables, channels, CSP, message passing, RPC, rendezvous, etc. These methods are good in practice as long as the discipline is maintained, but in large software systems, maintained over long periods by many different people, they tend to break down.

–  –  –

One family of techniques to help programmers write better quality software is formal methods, such as model checking, programming languages, type theories, and verification. As compared to testing, these methods require more theoretical and engineering machinery, but they can provide stronger guarantees, ensuring that programs behave properly even in tricky corner cases.

Each method has strengths and weaknesses. A typical model-checking method enumerates all possible scenirios under a certain size to produce a bound on program behavior. To reach a conclusion in a reasonable


 amount of time, a model-checker makes various kinds of simplifying assumptions that are unsound in certain, weakening the guarantees provided. New programming languages can be devised to help programmers write better code, but generally speaking, programmers are very reluctant to adopt new languages, or even new features in old ones.

Type systems, in which the types produce a conservative approximation for the result of the program, can have the major advantage of being almost entirely automated (that is, the computer can apply the type system without significant help from the programmer). However, type systems seldom provide the strongest kinds of guarantees. Finally, verification, a technique whose end goal is a formal mathematical proof that a program meets its specification, can produce the most expressive and powerful guarantees about system behavior, but can be very labor-intensive to do.

1.2.1 By Hand or Machine Reasoning about real code is very complex, frequently requiring dozens of special cases, exceptions, and assumptions to guarantee the desired behavior. Even for purely sequential programs, to apply a given formal method to a computer system can be quite difficult. There are two basic strategies for doing so.

–  –  –

One obvious problem is that features in the core can interact with other “noncore” features in surprising ways, meaning that properties proven to hold for the core might not hold for the whole system. This is a serious concern, although generally people are good at understanding which parts of the system are vital to the proof of the desired property. The real challange lies in implementing the system. Naturally, one takes as much care as possible to implement it correctly and avoid bugs. Unfortunately, if the system is of any significant size, it will have many bugs; one is hopeful, however, that they will not be too numerous or serious, and with careful testing one can have a program that is well-behaved most of the time.

The second strategy is to try to prove something about the actual code of the computer system. The challange is then to deal with all of the special cases, exceptions, assumptions, and other complexities involved in real code. The details can quickly become overwhelming if one is writing traditional pen-and-paper proofs. There is another possibility, however, which is to use a computer to help with the process.

Although there are many automated theorem checkers in existence, including Coq, Isabelle/HOL, and Twelf, using a computer to develop and check proofs is not easy. Generally speaking, a computer is better at proof checking than proof development (e.g., type checking is simpler than type inference). Some formal methods, such as the simpler type systems or model checking, have very significant automation possibilities, where the computer can do most or even all of the work. Other


 methods, such as verification, tend to only use automation to check proofs; fully automatic generation of verification proofs tends to be too difficult.

Pages:   || 2 | 3 | 4 | 5 |   ...   | 22 |

Similar works:

«Utilizing Soft Computing Methods in Analyzing Build-Operate-Transfer (BOT) Contracts Neda Shahrara Submitted to the Institute of Graduate Studies and Research in partial fulfillment of the requirements for the Degree of PhD in Civil Engineering Eastern Mediterranean University September 2015 Gazimağusa, North Cyprus Approval of the Institute of Graduate Studies and Research Prof. Dr. Serhan Çiftçioğlu Acting Director I certify that this thesis satisfies the requirements as a thesis for the...»


«Structure Investigations of Membrane Protein OEP16 by James Duncan Zook A Dissertation Presented in Partial Fulfillment of the Requirements for the Degree Doctor of Philosophy Approved May 2012 by the Graduate Supervisory Committee: Petra Fromme, Chair Julian Chen Rebekka Wachter ARIZONA STATE UNIVERSITY August 2012 ABSTRACT Membrane protein structure is continuing to be a topic of interest across the scientific community. However, high resolution structural data of these proteins is difficult...»

«Journal of Educational and Social Research ISSN 2239-978X Vol. 4 No.6 ISSN 2240-0524 September 2014 MCSER Publishing, Rome-Italy Igala Proverbs as Bastions of Societal Harmony Egbunu, Fidelis Eleojo (PhD) Department of Philosophy and Religious Studies, Kogi State University, Anyigba, Kogi State, Nigeria Email: frfidele@yahoo.com Doi:10.5901/jesr.2014.v4n6p259 Abstract This paper “Igala Proverbs as Bastions of Societal Harmony” is fundamentally a brisk quest into this all-interesting and...»

«INVESTIGATING STRUCTURE-FUNCTION RELATIONSHIPS IN FAMILY 7 CELLULASES BY MOLECULAR SIMULATION By Courtney Barnett Taylor Dissertation Submitted to the Faculty of the Graduate School of Vanderbilt University in partial fulfillment of the requirements for the degree of DOCTOR OF PHILOSOPHY in Chemical Engineering August, 2012 Nashville, Tennessee Approved: Clare McCabe Peter T. Cummings Eugene LeBoeuf Kenneth A. Debelak To Mom, Dad, John, and Mal, unwavering in their support and To Trent, for 13...»

«VERIFIABLE SEARCHABLE SYMMETRIC ENCRYPTION BY ZACHARY A. KISSEL B.S. MERRIMACK COLLEGE (2005) M.S. NORTHEASTERN UNIVERSITY (2007) SUBMITTED IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY COMPUTER SCIENCE UNIVERSITY OF MASSACHUSETTES LOWELL Signature of Author: Date: Signature of Dissertation Chair: Dr. Jie Wang Signatures of Other Dissertation Committee Members Committee Member Signature: Dr. Xinwen Fu Committee Member Signature: Dr. Tingjian Ge Committee...»

«The Effects of Multiple Discounts on Consumers’ Product Judgments A Thesis Submitted to the Faculty of Drexel University by Zhen (Jane) Cai in partial fulfillment of the requirements for the degree of Doctor of Philosophy June 2008 © Copyright 2008 Zhen (Jane) Cai. All Rights Reserved. ii DEDICATION This work is dedicated to Mom & Dad and Chao iii Acknowledgements This dissertation represents a continuous learning experience through which I have gained a deeper understanding of both the...»

«Representations of Gender and Subjectivity in 21st Century American Science Fiction Television Sophie Halliday Submitted for the degree of Doctor of Philosophy University of East Anglia, School of Film, Television and Media Studies March 2014 This copy of the thesis has been supplied on condition that anyone who consults it is understood to recognise that its copyright rests with the author and that use of any information derived there from must be in accordance with current UK Copyright Law....»

«On (Non)Factivity, Clausal Complementation and the CP-Field A Dissertation Presented by Carlos Francisco de Cuba to The Graduate School in Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy in Linguistics Stony Brook University August 2007 Stony Brook University The Graduate School Carlos Francisco de Cuba We, the dissertation committee for the above candidate for the Doctor of Philosophy degree, Hereby recommend acceptance of this dissertation Daniel L. Finer...»

«ABSTRACT Title of dissertation: DOSE RANGING STUDY OF LUTEIN SUPLEMENTATION IN ELDERLY WITH AND WITHOUT AGE RELATED MACULAR DEGENERATION Fabiana Fonseca de Moura, Doctor of Philosophy, 2004 Dissertation directed by: Professor Frederick Khachik Adjunct Professor, Department of Chemistry and Biochemistry and the Department of Nutrition and Food Science Age-related macular degeneration (AMD) is the leading cause of blindness among people over the age of 65. Epidemiological studies have indicated...»

«Developing a Framework to Improve Critical Infrastructure Cybersecurity Presented by Joe Wilson Network Security Engineer TelcoCapital IT Systems, LLC Dissertation Presented in Partial Fulfillment Of the Requirements for the Degree Doctor of Philosophy Cybersecurity Framework Development: Design Science Research toward an Intercloud Transparent Bridge Architecture (ITCOBRA) CAPELLA UNIVERSITY A National Center of Academic Excellence in Information Assurance Education (CAE/IAE) March 2013 © Joe...»

«WRITING BARCELONA: REFLECTIONS ON CITY PLANNING AND URBAN EXPERIENCE, 1854-1888 BY JORDI OLIVAR DISSERTATION Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy in Spanish in the Graduate College of the University of Illinois at Urbana-Champaign, 2010 Urbana, Illinois Doctoral Committee: Associate Professor Luisa-Elena Delgado, Chair Associate Professor Jordana Mendelson, New York University Associate Professor Joyce Tolliver Assistant Professor Ericka...»

<<  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.