FREE ELECTRONIC LIBRARY - Dissertations, online materials

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

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

-- [ Page 5 ] --

the Hoare tuple is defined using the various guards in a continuationpassing style8. There are many details here, which is common when building machine-checked proofs of large, realistic systems, but in simple terms, the Hoare tuple says that for any continuation κ, if the postcondition Q ensures the safety of κ, then the precondition P ensures the safety of c followed by κ.

Using this definition, Appel and Blazy prove, in Coq, soundness of the rules of sequential separation logic given in figure 2.6. The rules for skip, sequenceb, assignment, and loop are standard. The rule for storing the the heap requires that e and e2 be pure—that is, not read from the heap. Appel and Blazy demonstrate how to accommodate impure expressions by applying local program transformations. The if-then-else rule also requires that e be pure, which can be handled in closemod (s, A) closes the assertion A over any variables modified by s.



–  –  –

Figure 2.6: Axiomatic Semantics of Separation Logic (without call and return) the same way.

The block and exit rules enable reasoning for nonlocal control flow. Not pictured are the standard rules of separation logic such as the rule of consequence and the frame rule; also missing are the rules for call and return. For a full description of all of the rules and the consequences for sequential control flow we refer the reader to [AB07].

The proofs of these rules with respect to the definition of the Hoare tuple is done in Coq [AB07]. The most difficult rule to prove was the loop rule, which interacted complexly with the block and exit rules.

–  –  –

the memory model, and basic definitions, all of which are shared with CompCert. 19% is the definition of the C minor language and the model for permissions. 2% is the operators and rules of sequential separation logic, and the final 42% is the proofs of soundness for those rules.

Like the correctness proofs of the compiler, the proofs of the soundness of the separation logic rules make a number of assumptions about the underlying semantics. Unfortunately, just as in the compiler correctness proofs, several of the assumptions used, such as determinancy of the step relation, are typically false in a concurrent setting. The challenge when adding concurrency will be in a large part how to adapt these sequential-language proofs to a concurrent language.

In the remainder of this thesis, since the focus is not on sequential control flow, both the R and B parameters will be elided from the presentation. However, their existance forms a part of the motivation to design the concurrency system cleanly, which is why they were presented in full detail here: the Hoare tuple is complex enough to begin with, and there is every reason to avoid making it any more complicated than it already is.

–  –  –

With the combination of Appel and Blazy with the work of Leroy, it is possible to create an end-to-end guarantee: properties proven of the source code using separation logic will hold on the code that executes on the machine. Moreover, since the entire system is machine-checked endCHAPTER 2. RELATED WORK  to-end, there is very high assurance that the actual program written, when run through the actual compiler used, will actually behave as specified in the source code.

2.6 Generation of proofs in CSL One issue not yet discussed is where the proofs in CSL come from. One obvious possibility is that they are generated by humans, ideally in some machine-checked setting, as the code is being written. However, this can involve a great deal of additional effort if it is done directly, even considering that the amount of debugging time is dramatically less.

Appel [App06] presents one way to make the process simpler by giving a series of custom Coq tactics for reasoning about C minor programs in Coq. Using these tactics it is possible for a human to generate a proof more easily.

Another approach is given by Gotsman et al. [GBCS07]. Gotsman develops a separation-logic-based shape-analysis algorithm that can automatically generate correctness proofs for certain classes of simple concurrent programs.

Mansky [Man08] uses both approaches. First he takes a relatively

–  –  –

In general humans are able to verify very complex programs, but it takes an enormous amount of effort. In contrast, automatic techniques can only handle relatively simple cases, but are able to do so with great efficiency. Clearly a reasonable approach is to combine the two, letting humans handle the difficult parts of a program while using powerful inference techniques to automate the analysis of the simpler parts, but exactly how to do make everything fit together is an open problem.

2.7 Gotsman et al.’s CSL Gotsman et al. independently developed a version of concurrent separation logic [GBC+ 07]. Their CSL is similar to ours, indicating that we

have independently discovered the natural extension of CSL to firstorder locks. Key differences between their work and ours include:

1. Our assertion language is more powerful, providing support for features such as impredicative quantification, higher-order recursion, and first-class function pointers. We are able to use this power to define very powerful assertions, such as the Hoare tuple, and check programs in a more modular way.

2. We can embed our assertions directly into the syntax of programs, while they must utilize a global table on the side.

–  –  –

velop our system in a highly modular way: the sequential reasoning is isolated from the concurrent reasoning in the model, and the isolation is strong enough to make the proof in Coq tractable.

This modularization leads to a very different flavor of soundness proof: while they argue via predicate transformers, we establish soundness in a more operational style.

4. We have a strategy for connecting to an existing certified compiler, and a thesis for why our results should hold on a machine with a weak memory model, thereby achieving an end-to-end system.

5. Gotsman’s system is designed to connect to the shape analysis tool presented in [GBCS07].

6. Gotsman also presents a method for guaranteeing that all locks

–  –  –

We suspect that it would not be difficult to extend our work to support (6). One interesting avenue for future work would be to combine the positive aspects of the two approches, thereby achieving both (4) and (5) and an even larger end-to-end system.


2.8 Miscellaneous related work 2.8.1 A very modal model Our semantic model for assertions was built on top of ideas first developed for the Princeton Foundational Proof-Carrying Code project for modeling mutable references [AM01, AAV02, AAV03, Ahm04]. Appel et al. [AMRV07] re-engineered this model by developing a modal logic with an underlying Kripke model to achieve greater modularity.

2.8.2 The C0 compiler Leinenbach et al. [LPP05] developed the C0 certified compiler. C0, like C minor, is a simplified version of the C language, and the C0 compiler translated C0 into the DLX machine language. This compiler was part of the larger Verisoft project, which built an entire machineverified hardware/software stack, from the gate level through a TCP/IP stack. The verification was done in Isabelle/HOL. In comparison to the CompCert compiler, the C0 compiler is simpler, supporting very few optimizations.

2.8.3 Release Consistency Release consistency, proposed by Gharachorloo et al. [GLL+ 90], is a memory consistency model first proposed in the systems/architecture community in 1990. This work was one of the first to demonstrate the


 benefits of distinguishing lock/unlock memory accesses from ordinary loads and stores; we follow them in this regard.

Synchronization actions are guaranteed to be sequentially consistent, while normal accesses are not, with the exception that they must execute with respect to synchronization actions in program order. Assuming proper synchronization (similar in nature to that required by CSL), release consistency is consistent with sequential consistency; our thesis for why our system should be sound in the presence of weak memory models is similar.

Chapter 3 Concurrent C minor Concurrent C minor is a new high-level intermediate language suitable for writing concurrent programs. Here we present the new language, give an informal semantics, and present an example. Later we give three different formal semanics for Concurrent C minor. First, in chapter 5, we give a simple concurrent operational semantics to demonstrate that we support a standard model for concurrent programming. Second, in chapter 8, we present a more complicated concurrent operational semantics that does additional bookkeeping to allow us to prove strong properties. Last, in chapter 9, we give an oracular semantics, which is a thread-local semantics for concurrent execution1.

Portions of this chapter have been published before as [HAZ08a] and [HAZ08b].

–  –  –

The Concurrent C minor language is built on top of the (sequential) C minor language first developed by Leroy [Ler06] and then modified by Appel and Blazy [AB07]. The sequential features include: complex control flow, such as function calls and multi-exit loops; support for the full ANSI C memory model, including pointer arithmeric and the ability to work with variable-sized data2 ; and certain other features useful in an intermediate language such as locally nameless variables.

In figure 2.3 we gave the grammar of Appel and Blazy’s version of C minor, which we extend here.

We extend C minor with five statements to construct Concurrent C

minor :

–  –  –

always passes to the next statement in the program.

The lock (e) statement evaluates e to an address v, then waits until it acquires lock v. The unlock (e) statement evaluates e to an address v and then releases the lock v. A lock at location v is locked when the memory contains a 0 at v and unlocked when memory contains a 1 at v.

Each lock comes with a resource invariant R which is an assertion that explains how the lock should be used and which addresses in memory it owns. R must hold before unlocking a lock, which means the next thread to grab the lock will know that R holds. This is standard in CSL [O’H07], but we go further and use the invariants at a crucial point in our unerased concurrent operational semantics to guarantee the absence of race conditions.

The unerased concurrent operational semantics checks the truth of lock invariants when unlocking a lock; failure of this check causes the operational semantics to get stuck, as explained in in chapter 8. The language of these assertions contains the full power of logical propositions (Coq’s Prop), so the operational semantics is nonconstructive, i.e., it is given by a classical relation3.

The set of memory locations controlled by a lock need not be static;

it can change over time depending on the state of memory (e.g., one can say, “this lock controls that variable-sized linked list”). As explained in section 2.5.2, if a thread tries to access memory it does not own, it gets We use a small, consistent set of classical axioms in Coq: extensionality, proposition extensionality, dependent unique choice, and relational choice.


 stuck. This protocol ensures the absence of read/write or write/write race conditions.

The statement make lock e R takes an address e and a lock invariant R, and declares e to be a lock with the associated invariant. make lock will get stuck if memory location e does not contain a 0, meaning that the lock is created in the locked state. The address is turned back into an ordinary location by free lock e, which also requires the location e to contain a 0. Both instructions are thread-local, i.e., they don’t synchronize with other threads or the scheduler. It is illegal to apply lock or unlock to nonlock addresses, or to apply ordinary load or store to locks.

The fork statement spawns a new thread, which calls function e on arguments e. No variables are shared between the caller and callee except through the function parameters. All functions in Concurrent C minor are given pre- and postconditions, and the parent passes to the child a portion of the memory it controls, specified by the precondition of the child. This portion typically contains visibility of some locks so that the two threads can communicate. Just as the operational semantics gets stuck at unlock if the lock invariant does not hold, it will get stuck at fork if the child’s precondition does not hold. A thread exits by returning from its top-level function call.

–  –  –

Although the syntax of Concurrent C minor requires the user to specify lock invariants and function pre- and postconditions, these can be taken directly from a program proof in concurrent separation logic.

Therefore, if the author of a Concurrent C minor program wishes to develop a verified program, it is not an extra burden to augment the source code with the appropriate invariants.

3.2 Programming with locks To illustrate programming in Concurrent C minor, we give an example program in figure 3.1. Here we explain the program’s behavior and present an informal proof that it is bug-free. For cross-referencing purposes we number both the lines of the program in figure 3.1 and the informal proof.

i. Every program in Concurrent C minor has a special function main, where the program begins. In Concurrent C minor, at function declaration it is necessary to give pre- and postconditions.

In the example program, main is declared in line 1, and both the pre- and postconditions are declared to be emp. The assertion language for pre- and postconditions is explained in section 4;

the emp precondition indicates that main can be run at any time, and the emp postcondition indicates that when main terminates

–  –  –

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

Similar works:

«c 2012 Vijay Raman TRAFFIC-AWARE CHANNEL ALLOCATION AND ROUTING IN MULTICHANNEL, MULTI-RADIO WIRELESS NETWORKS BY VIJAY RAMAN DISSERTATION Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy in Electrical and Computer Engineering in the Graduate College of the University of Illinois at Urbana-Champaign, 2012 Urbana, Illinois Doctoral Committee: Professor Nitin Vaidya, Chair Assistant Professor Matthew Caesar Assistant Professor Sayan Mitra Professor...»

«PROBLEMS AND CHALLENGES Faced by Liberian Refugee Children and Youths as they enter the formal Educational Systems at the Buduburam Refugee Camp in Ghana TIEN KEAH BORTU A thesis submitted in fulfillment of the requirement for the degree of Master of Philosophy in Comparative and International Education INSTITUTE FOR EDUCATIONAL RESEARCH, FACULTY OF EDUCATION UNIVERSITETET I OSLO SPRING 2009 ABSTRACT This study addresses the challenges that Liberian refugee children and youths living at the...»

«From Greenhouse to Icehouse: Understanding Earth’s Climate Extremes Through Models and Proxies Clay Richard Tabor A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Geology) in the University of Michigan Doctoral Committee: Professor Chris J. Poulsen, Chair Associate Professor Jeremy N. Bassis Associate Professor Brian K. Arbic Senior Scientist David Pollard Acknowledgements Foremost, I would like to thank my advisor Chris Poulsen for...»

«DO NORMATIVE JUDGEMENTS AIM TO REPRESENT THE WORLD? Bart Streumer b.streumer@rug.nl Ratio 26 (2013): 450-470 Also in Bart Streumer (ed.), Irrealism in Ethics Published version available here: http://dx.doi.org/10.1111/rati.12035 Abstract: Many philosophers think that normative judgements do not aim to represent the world. In this paper, I argue that this view is incompatible with the thought that when two people make conflicting normative judgements, at most one of these judgements is correct....»

«Understanding Civic Engagement among Youth in Diverse Contexts By Holly Lynn Karakos 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 Community Research and Action May, 2015 Nashville, Tennessee Approved: Maury Nation, Ph.D. Andrew J. Finch, Ph.D. Paul Speer, Ph.D. Sonya Sterba, Ph.D. ABSTRACT Research suggests that youth civic engagement is beneficial for individuals and...»

«University of Alberta From Prohibition to Administrative Regulation: The Battle for Liquor Control in Alberta, 1916 to 1939 by Sarah Elizabeth Mary Hamill A thesis submitted to the Faculty of Graduate Studies and Research in partial fulfillment of the requirements for the degree of Doctor of Philosophy Faculty of Law ©Sarah Elizabeth Mary Hamill Spring 2014 Edmonton, Alberta Permission is hereby granted to the University of Alberta Libraries to reproduce single copies of this thesis and to...»

«Downloaded from http://rsnr.royalsocietypublishing.org/ on November 18, 2016 Notes Rec. R. Soc. doi:10.1098/rsnr.2009.0051 Published online LINNAEUS AND CHINESE PLANTS: A TEST OF THE LINGUISTIC IMPERIALISM THESIS by ALEXANDRA COOK* Department of Philosophy, University of Hong Kong, Pokfulam Road, Hong Kong S.A.R. It has been alleged that Carolus Linnaeus practised Eurocentrism, sexism and racism in naming plant genera after famous botanists, and excluding ‘barbarous names’. He has therefore...»

«DESIGN OF FAULT TOLERANT CONTROL SYSTEMS by Benjamin Erik Walker A dissertation submitted to the faculty of The University of North Carolina at Charlotte in partial fulfillment of the requirements for the degree of Doctor of Philosophy in Electrical Engineering Charlotte 2012 Approved by: Dr. Bharat Joshi Dr. Yogendra Kakad Dr. James Conrad Dr. Mehdi Miri Dr. Edgar Munday ii ©2012 Benjamin Erik Walker ALL RIGHTS RESERVED iii ABSTRACT BENJAMIN ERIK WALKER. Design of fault tolerant control...»

«A study on the control of NOx and Particulate Matter emissions from Dimethyl Ether combustion in compression ignition engines George Thomas B.Tech, M.E, M.Phil (Mechanical Engineering) A thesis submitted for the degree of Doctor of Philosophy at The University of Queensland in 2015 School of Mechanical and Mining Engineering i Abstract Dimethyl Ether (DME) is a new age fuel developed mainly from coal and natural gas to use in compression ignition (CI) engines relatively easily with minimum...»

«Becoming Joaquin Murrieta: John Rollin Ridge and the Making of an Icon By Blake Michael Hausman A dissertation submitted in partial satisfaction of the requirements for the degree of Doctor of Philosophy in English in the Graduate Division of the University of California, Berkeley Committee in charge: Professor Hertha D. Sweet Wong, Chair Professor Bryan Wagner Professor Beth H. Piatote Fall 2011 1 Abstract Becoming Joaquin Murrieta: John Rollin Ridge and the Making of an Icon by Blake Michael...»

«Creating Green Chemistry: Discursive Strategies of a Scientific Movement Jody A. Roberts Dissertation submitted to the Faculty of Virginia Polytechnic Institute and State University in partial fulfillment of the requirements for the degree of Doctor of Philosophy in Science and Technology Studies Committee: Richard M. Burian (chair) Daniel Breslau Richard F. Hirsh Timothy W. Luke Joseph C. Pitt 13 December 2005 Keywords: Green Chemistry, Scientific Movements, Chemistry Studies, Discursive...»

«Studying Physical Properties at the Nano-Scale: Thin Films, Nano-Particles and Molecules by Alon Eisenstein A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Department of Chemistry University of Toronto © Copyright by Alon Eisenstein 2014 Studying Physical Properties at the Nano-Scale: Thin Films, Nano-Particles and Molecules Alon Eisenstein Doctor of Philosophy Department of Chemistry University of Toronto Abstract Nanomaterials have been shown to...»

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