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



Pages:     | 1 | 2 || 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 3 ] --

Eigthth, to gain confidence that our new CSL is well-defined, we

CHAPTER 1. INTRODUCTION

 must develop a soundness proof for it, connecting it to our concurrent operational semantics. However, connecting it directly is messy. Instead, we define a new oracular semantics, which looks and behaves sequentially, but is able to proceed at concurrent instructions. This semantics will be so sequential that we will be able to use definitions and proofs developed in purely sequential settings with it, and properties proven in the oracular setting will then carry over into the concurrent one. The oracle semantics and its soundness proof is developed in chapter 9.

Nineth, we connect our new CSL to our oracle semantics. To do this we must define the Hoare triple in terms of the oracular operational semantics, and then prove the CSL axioms as lemmas from that definition. We are greatly aided by being able to connect to the oracle semantics, which lets us largely re-use a definition for the Hoare triple first developed in the sequential setting by Appel and Blazy. Using this imported definition we are able to recycle their proofs of all of the rules of CSL that come from SSL (which constitute a majority of the rules of CSL). For the rules about the concurrent features, such as the lock rule, we develop the proof from scratch but are able to ignore the sequential features while arguing about concurrent behavior. Our definition of the Hoare triple and the proofs of the CSL rules is presented in chapter 10.

Tenth, we present areas for future research. These include modifying the CompCert compiler to handle concurrency, developing techniques to reason about lock-free algorithms of various kinds, and reasonSTRUCTURE OF THESIS  ing in the presence of weak memory models. We conclude by observing that this system would allow for end-to-end reasoning of programs, from the source code to the machine code, all in a machine-checked manner.

Our view on future work and concluding thoughts are contained in chapter 11.

Chapter 2 Related Work

2.1 Hoare logic and separation logic Hoare logic is a verification technique developed by Hoare and Floyd to verify the behavior of a program [Flo67, Hoa69]. A Hoare triple is a judgement of the form {P } c {Q}, where P and Q are assertions and c is a command. Assertions are formulas in some logic, and the command c is a statement in a programming language. P is usually called the precondition, and Q the postcondition. The informal meaning of a Hoare triple is “If P holds, then after one executes c, Q will hold.” A Hoare logic is a set of triples, called axioms or rules. Typically

these contain free variables, which are universally quantified. For example:

–  –  –

The sequence rule says that it is valid to chain together sequences of assertions, allowing for pre- and postconditions for groups of statements, functions, and whole programs. It certainly seems like a reasonable rule—however, it is usually not true in concurrent setings! Another thread could modify the state after c1 has executed, invalidating the postcondition R, thus invalidating any guarantee about the state after c2 executes. This is an indication of why moving from sequential to concurrent settings is difficult.

–  –  –

If a Hoare logic is simply a set of axioms, how does one determine which sets of axioms are reasonable? In other words, consider the following

two possible axioms:

–  –  –

Which one is correct? On first inspection, the first one seems much more likely to be correct than the second. However, the true answer depends on what it means for an assertion such as {x = 0} to hold, what pre- and postconditions are, and the result of the command x++.

For example, many garbage-collected languages use a “tag bit”: that is, if the lowest bit in an integer value is 0, then that value is regular data; if on the other hand the lowest bit is 1, then that value is a pointer. In that case, all integer calculations would be carried out using only the upper 31 bits. If the logic was designed to reason about this issue (which would be important if one was trying to verify the garbage collector in question), then in fact axiom 2 would be the correct rule.

Perhaps for simple languages, one can simply “eyeball” the rules, but for languages with complex features more is required.

A soundness proof is needed to demonstate that a particular set of axioms is valid. A soundness proof of an axiomatic semantics like Hoare logic is a connection between the definitions of “assertion,” “precondition,” “postcondition,” and the operational semantics of the language in question. To make this connection, a formal definition is given to the Hoare triple, and the Hoare axioms are proven as lemmas from that definition.

Despite the importance of establishing soundness, hereafter, for ease of presentation, statements have the “obvious” semantics unless otherwise specified.

CHAPTER 2. RELATED WORK

 2.1.2 Separation Logic One problem with Hoare logic is that it is difficult to use it to reason

about pointers, due to aliasing. Consider the judgment:





–  –  –

Here, the notation a → b means that a is a pointer and is pointing to a memory location that contains the value b. The question is, what is the correct postcondition? One obvious candidate is x → 1 ∧ y → 0, but it is not the only candidate: there is also x → 1 ∧ y → 1, since x and y could be aliased —that is, they could point to the same location in memory. In that case, updating [x] would also update [y]. This ambiguity causes the logic to be unsound (that is, a property “proven” using the logic might not actually hold when the program is executed).

This is exactly the kind of subtle problem a soundness proof prevents.

There are a variety of possible solutions to the problem of aliased pointers. For example, one could include the explicit requirement that

x and y not be aliased:

–  –  –

The benefit of this approach is that with the restrictions on aliasing in place, the logic becomes sound once again. However, the number of aliasing constraints grows quadratically with the number of locations. In

2.1. HOARE LOGIC AND SEPARATION LOGIC  some contexts this may not be a problem, but often the detail becomes overwhelming.

Separation logic, developed by Reynolds and O’Hearn, gives a more abstract, cleaner view of the problem2 [Rey02, IO01]. The key idea is to add a new operator, the separating conjunction ∗, to the assertion logic. P ∗ Q means that P and Q hold on disjoint sections of memory.

This means that updates to the part of memory described by P cannot affect the validity of Q, and vice versa. Using this new operator, we can

phrase our initial axiom in a different way:

–  –  –

The advantage of presenting things this way is that the aliasing constraints are bundled up in the ∗ operator, and thus do not overwhelm the reasoning.

The key to understanding the power of the separating conjunction

–  –  –

The frame rule says that if one has proven the validity of some statement “in a vacuum,” then it is valid to add it to a larger program, even if the other parts of the program place restrictions on parts of memory untouched by the statement in question. It thus supports local reasonAs mentioned in chapter 1, since this work focuses on concurrency, separation logic that does not handle concurrency will be called sequential separation logic (SSL).

CHAPTER 2. RELATED WORK

 ing by allowing verifiers to concentrate on the parts of the state being modified by the statements under consideration. One critical point is that the frame rule is not true if one substitutes the normal conjunction

for the separating one:

–  –  –

This rule is unsound because F could be describing some of the same memory described by P and modified by c.

2.2 Concurrent Separation Logic Another problem with Hoare logic is that it is difficult to use it to

reason about concurrency. Consider again the sequence rule:

–  –  –

As mentioned above, this rule is usually false in a concurrent setting because the action of other threads executing between c1 and c2 can invalidate the postcondition R of c1 before c2 can execute. If R does not hold, then there is no gurantee that c2 ’s will result in the postcondition Q, making this rule unsound. A soundness proof would prevent subtle problems resulting from such a rule.

–  –  –

Here, c1 c2 indicates that the statements c1 and c2 are to be executed concurrently. If each thread is operating on its own part of memory (which is guaranteed by the separating conjunction), then it is valid to reason about them independently.

CSL includes all of the rules of SSL for verifying the individual threads—that is, the rules of SSL are a proper subset of the rules of CSL. This means that CSL includes the sequence rule, which typically is unsound in concurrent settings. Informally, the sequence rule is sound because all the threads are operating on disjoint parts of memory. Thus, when executing the sequence c1 ;c2, any postcondition R of c1 cannot be invalidated by the action of any other thread, meaning that it will be valid to use R as the precondition of c2.

Verifying a program with CSL not only allows local reasoning, thereby avoiding significant space blow-up, but also allows for the direct re-use of SSL verifications, since all of the rules of SSL are in CSL. This second benefit is a significant advantage, since verification can be extremely

CHAPTER 2. RELATED WORK

 labor-intensive.

2.2.1 Thread Communication The parallel rule allows two processes to run independently, but says nothing about how processes collaborate. To achieve collaboration, which is an important part of concurrent programming, additional rules and semantics are needed.

The synchronization device used in CSL is the lock, also called a resource. In O’Hearn’s CSL, resources are declared statically at the beginning of a program, and in the verification each resource r is associated with a resource invariant RI r.

To use the resource r, O’Hearn provides the critical section rule:

–  –  –

When inside the critical section, the code may use not only the thread’s private memory, but also the memory controlled by the resource. The critical region c can proceed only when it has exclusive access to the resource r and the boolean value B is true. The side condition involving other processes may seem very strong; it is necessary because in O’Hearn’s CSL, local variables are shared between processes. The separating conjunction ensures that memory is divided appropriately, but does not say anything about the local variables.

2.2. CONCURRENT SEPARATION LOGIC  2.2.2 Limitations to the Approach Despite the significant advantages of the approach, as originally presented, CSL had several drawbacks. First, several of the features of the language for which CSL was developed were not standard. The parallel composition operator and the critical section construct are more static and less general than dynamic commands such as fork to start parallel computation in an open-ended manner, and lock and unlock for synchronization purposes. In other words, it is straightforward to use fork, lock, and unlock to implement and with-when-do; however it is not obvious how to do the opposite.

Second, the idea of sharing local variables between threads is problematic. Local variables are typically compiled to registers, and registers are not shared between threads by the context-switching mechanism.

This makes shared local variables in a language questionable. In addition, one unfortunate result of sharing local variables is the second premise of the critical section rule, which places requirements on other processes and therefore has more of a global flavor than might be hoped.

Third, CSL lacked first-class locks. As mentioned above, in O’Hearn’s CSL, all locks are statically declared at the beginning of the program, and cannot be created once the program has begun. Programming in this style is frequently unnatural, and in many real programming languges, particularlly in object-oriented languages, locks are created and destroyed constantly as programs execute. Dynamic first-class locks were not included in CSL because it was unclear how to prove them

CHAPTER 2. RELATED WORK

 sound; indeed they were regarded as a significant technical challenge,

as indicated by Bornat et al. [BCOP05]:

...the idea of semaphores in the heap makes theoreticians wince. The semaphore has to be available to a shared resource bundle: that means a bundle will contain a bundle which contains resource, a notion which makes everybody’s eyes water. None of it seems impossible, but it’s a significant problem, and solving it will be a small triumph.

Fourth, CSL did not have function pointers. Actually, the original CSL did not even have functions! First order functions (i.e., functions that could not be passed as arguments or protected by locks) would not cause any fundamental problems, but it was thought [O’H07, §4] that they would complicate the soundness proof, a good example of why a machine-checked proof is so important when reasoning about more realistic systems. However, first class functions and function pointers are a considerably harder problem for the same kinds or reasons that first-class locks are a harder problem than static locks.



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


Similar works:

«REPRESENTING TERRORISM: AESTHETIC REFLECTION AND POLITICAL ACTION IN CONTEMPORARY GERMAN NOVELS (GOETZ, KLEIN, TELLKAMP) By Mark Einer Looney 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 German May, 2010 Nashville, Tennessee Approved: Professor Christoph Zeller Professor Barbara Hahn Professor Meike Werner Professor Gregg Horowitz Copyright © 2010 by Mark Einer Looney...»

«UCGE Reports Number 20185 Department of Geomatics Engineering An Analysis on the Optimal Combination of Geoid, Orthometric and Ellipsoidal Height Data (URL: http://www.geomatics.ucalgary.ca/links/GradTheses.html) by Georgia Fotopoulos December 2003 UNIVERSITY OF CALGARY An analysis on the optimal combination of geoid, orthometric and ellipsoidal height data by Georgia Fotopoulos A THESIS SUBMITTED TO THE FACULTY OF GRADUATE STUDIES IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF...»

«Imperfect Partnership: Effects of Collaboratories on Scientists from Developing Countries by Airong Luo A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Information) in The University of Michigan Doctoral Committee: Professor Judith S. Olson, Chair Professor Michael D. Cohen Associate Professor Fiona Lee Assistant Professor Steven Jackson Copyright airong Luo All rights reserved DEDICATION For Eleanor and Evan Park ii ACKNOWLEDGEMENTS I...»

«Mothering in the Context of Criminalized Women’s Lives: Implications for Offending by Carolyn F. Yule A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy, Department of Sociology, University of Toronto © Copyright by Carolyn Yule (2010) Mothering in the Context of Criminalized Women’s Lives: Implications for Offending Carolyn Yule Doctor of Philosophy Department of Sociology University of Toronto Abstract While it is widely known that most women...»

«Forensic Taphonomy: Investigating the Post Mortem Biochemical Properties of Cartilage and Fungal Succession as Potential Forensic Tools A thesis presented for the degree of Doctor of Philosophy Shawna N. Bolton, B.A. (Hons.), M.Sc. University of Wolverhampton Faculty of Science and Engineering PhD Supervisors: Dr Michael Whitehead and Dr Raul Sutton ii iii Abstract Post mortem interval (PMI – the time elapsed since death and discovery) is important to medicolegal investigations. It helps to...»

«MEDIA NARCISSISM AND SELF-REFLEXIVE REPORTING: METACOMMUNICATION IN TELEVISED NEWS BROADCASTS AND WEB COVERAGE OF OPERATION IRAQI FREEDOM By ANDREW PAUL WILLIAMS 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 2004 by Andrew Paul Williams This dissertation is dedicated to my parents. I owe a great deal of gratitude to my mother, Lois Virginia Strickland...»

«Fundamental Investigations of Anhydrous Metal Dodecaborates for Energy Applications A Dissertation Submitted for the Degree of Doctor of Philosophy Author: He Liqing Supervisor: Akiba Etsuo 2015 Fukuoka, Japan Fundamental Investigations of Anhydrous Metal Dodecaborates for Energy Applications A Dissertation Submitted to Engineering of KYUSHU UNIVERSITY in Partial Satisfaction of the Requirements for the Degree of Doctor of Philosophy By He Liqing DEPARTMENT OF HYDROGEN ENERGY SYSTEMS GRADUATE...»

«FRAMING IMMIGRATION: THE IMPACT OF 9/11 AND THE LONDON TRAIN BOMBINGS ON THE PORTRAYALS OF IMMIGRANTS AND IMMIGRATION IN THE PRINT MEDIA By BEAU NILES 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 © 2010 Beau Niles ACKNOWLEDGEMENTS I would like to thank my committee chair Dr. Alin Ceobanu for his support and guidance through the process developing this project....»

«OPTICAL DEVICES AND SYSTEMS IN HIGHLY NONLINEAR MATERIALS AND GEOMETRIES by Daniel Hugh Broaddus This thesis/dissertation document has been electronically approved by the following individuals: Gaeta,Alexander L. (Chairperson) Lipson,Michal (Minor Member) Xu,Chunhui (Additional Member) OPTICAL DEVICES AND SYSTEMS IN HIGHLY NONLINEAR MATERIALS AND GEOMETRIES A Dissertation Presented to the Faculty of the Graduate School of Cornell University In Partial Fulfillment of the Requirements for the...»

«How can we explain the emergence of a language which benefits the hearer but not the speaker? Marco Mirolli1,2, Domenico Parisi1 1 Institute of Cognitive Sciences and Technologies, National Research Council 15, Viale Marx, 00137 Rome, Italy domenico.parisi@istc.cnr.it 2 Philosophy and Social Sciences Department, University of Siena 47, Via Roma, 53100 Siena, Italy mirolli2@unisi.it 1. Introduction 1.1 The problem Language requires the co-evolution of both speakers and hearers. i.e., the...»

«Zinc Oxide Transparent Thin Films For Optoelectronics by Karthik Sivaramakrishnan A Dissertation Presented in Partial Fulfillment of the Requirements for the Degree Doctor of Philosophy Approved November 2011 by the Graduate Supervisory Committee: Terry L Alford, Chair Dieter K Schroder Nathan Newman David Theodore ARIZONA STATE UNIVERSITY December 2010 ABSTRACT The object of this body of work is to study the properties and suitability of zinc oxide thin films with a view to engineering them...»

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





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