FREE ELECTRONIC LIBRARY - Dissertations, online materials

Pages:     | 1 |   ...   | 5 | 6 || 8 | 9 |   ...   | 22 |

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

-- [ Page 7 ] --

–  –  –

The simplest model for fractional permissions is a rational number in [0, 1]. A 0 means that neither reading nor writing are allowed; any nonzero means that reading is allowed; and a 1 gives permission to write—so permission for writing implies permission for reading. In this simple model, the join relation is addition if the total is less than or equal to 1, and two shares which sum to more than 1 do not join.

The existence of the unique identity element has been proven in Coq.

Just as with joinable types, in the Coq development, an uglier set of axoims than (8)–(12) is used. It has been proven in Coq that the presented axioms imply the ones used in the Coq development, with one minor exception: in the Coq development, the full and empty shares are explicitly constructed, instead of being shown to exist existentially. This explicit construction is useful for engineering purposes.


 As Parkinson explains in [Par05, ch. 5], this simple share model is not really sufficient for many applications. Among other problems, we cannot distinguish which half of the interval [0, 1] is owned because two shares both equal to the same rational number are indistinguishable.

To model this finer distinction, Parkinson proposed that a share be a subset of the natural numbers. The full share is then N, and the empty share the empty set. The join relation becomes the disjoint union operation10. Using this model, one can easily distinguish partial shares—two shares are equal only if the underlying sets are equal.

One drawback to using Parkinson’s model for our work is that it does not support the splitting axiom, since Parkinson allows finite subsets. The natural strategy for modifying Parkinson’s model to support the splitting axiom is to require that shares be infinite subsets of the naturals. Unfortunately, infinite subsets of the naturals do not support the intersection axiom, since the intersection of two infinite sets can be finite.

One mathematically elegant solution is to define a share to be an equivalence class of sets of real numbers taken from the interval [0, 1], where two sets are in the same equivalence class if their symmetric difference has Lebesgue measure of 0. The join relation of two shares π1 and π2 is defined as long as

–  –  –

If we write π to be the equivalence class containing S1 ∪ S2, then π1 ⊕ π2 = π. The join relation defined in this way will have all of the desired properties.

The problem with this model is that although it is mathematically clean, it would require developing measure theory in Coq, which is a sizable amount of work. A somewhat mathematically uglier technique is to define a share as the disjoint union of half-open intervals (open at the top) with rational endpoints drawn from the set [0, 1), and to define the join operation as the disjoint union operation on sets. One advantage of this model is that it only uses the reals implicitly, since it manipulates only the rational endpoints. However, it still proved difficult to implement in Coq11.

A third similar idea to use equivalence classes of reals where two sets are equivalent if their symmetric difference is countable. This is probably sufficient, but it was never implemented in Coq due to a general desire to avoid utilizing the real numbers unless absolutely necessary.

Using equivalence classes of naturals where two sets are equivalent if their symmetric difference is finite might also work, but has not been extensively developed.

Dockins [Doc08] developed a share model in which a share is modeled by a binary-tree data structure. Models developed from a computer science perspective are sometimes easier to model in Coq than models In fact, it was so painful that for most of the development time shares were simply infinite subsets of the naturals, even though this meant that the intersection property was false.


 developed from a mathematical perspective. Dockins’s model satisfies all of our axioms, and is currently being used in the Coq development.

To simplify the remainder of the presentation we will use the following convention. ◭◮ indicates the full share12, and ⊳⊲ indicates an empty share. Given a share π, we write ⌊π⌋ to indicate the “left half” of split(π) and ⌈π⌉ to indicate the “right half”; by the splitting rule, as long as π is not the empty share, then neither are ⌊π⌋ or ⌈π⌉. The left and right halves of the empty share are the empty share13 : ⌊⊳⊲⌋ = ⌈⊳⊲⌉ = ⊳⊲.

For the convienece of notation, we will write ◭⊲ for ⌊◭◮⌋ and ⊳◮ for ⌈◭◮⌉. Therefore,

–  –  –

associated with an assertion (in CSL) R, called the resource invariant of l. Just as with a maps-to assertion, we require that the share π be nonempty. A location cannot be both a normal memory cell and a lock. This restriction is enforced by not allowing a lock assertion and a

–  –  –

4.7.1 Resource invariants The resource invariant R of a lock l must hold before a thread can unlock the lock l, or the machine will get stuck. This means that the next thread to lock l will know that R holds. Locks are an exclusive form of access control, meaning that only one thread can hold a lock at a given time. Therefore, the thread that grabs the lock will know that no other thread will be able to touch the resource until the lock is unlocked again.

Resource invariants for locks must be closed to local variables, precise, and valid. An invariant R is closed to local variables when R does not depend on the values of the C minor locals. Since local variables are not usually shared in concurrency, this restriction is natural14.

An invariant R is precise when for all Q, the separating conjunction can only divide R ∗ Q in one way. An example of a precise predicate is a maps-to predicate. Requiring precision substantially simplifies the reasoning and lets the system be deterministic15, and moreover is part of the standard presentation of CSL [O’H07].

The notion of validity is technical and will be deferred until chapter

7. However, in practice validity is not a difficult requirement to satisfy On the other hand, Concurrent C minor can express the idea of memoryresident local variables, by permitting each function invocation to have a stackallocated memory block. Locations in these blocks can be addressed using load/store, and can be the subject of “maps-to” assertions. Stack-allocated addresses can be shared via the resource invariants of CSL. Before returning from a function, the thread must reclaim exclusive ownership of its stack block or the return command will get stuck.

It is unclear what kinds of trade-offs are possible if one wishes to relax the precision requirement; Gotsman has recently been working in this area [Got08].


 because all the operators mentioned above as being exposed to the user, as well as all the operators presented in section 4.7 are valid.

If an assertion R is closed, precise, and valid, then we say that R is tight. But how should we ensure that the user of our concurrent separation logic will always provide tight predicates? One choice is having side conditions, but this turns out to be annoying in the proofs. Instead, we utilize the new operators close, precisely, and validly. For all R, close R is closed, and moreover if R is closed, then close R = R. If R is not closed, then the meaning of the assertion close R depends on R and can be difficult to predict; in many cases it becomes false. precisely R and validly R are defined similarly with respect to precision and validity.

The formal definitions of close, precisely, and validly are technical and so are deferred until section 7.3.8.

We define tightly as the composition of validly, close, and precisely:

tightly R = validly (close (precisely R)). As expected, for all R, tightly R is tight, and tightly R = R if and only if R is tight16.

Using these definitions, it is possible to avoid stating explicit side conditions in the following way: when a lock with invariant R is unlocked, tightly R must hold; the next locking thread will then know tightly R holds after sucessfully acquiring the lock. If R is not tight, then the meaning of tightly R depends on R and is difficult to predict.

Frequently it will be equal to false; in this case it will be impossible to The definition of tightly is somewhat subtle; for example, exchanging the order of the composition leads to a bad definition, because precision is a less orthogonal property than one might hope for.

4.7. NEW ASSERTIONS FOR CSL  unlock the lock.

–  –  –

Partial ownership of a lock is sufficient to attempt to lock it. A thread that succeeds in locking a lock also gains the additional permission hold e R, which means that the expression e evaluates to a lock location l, with associated invariant R, and that the lock l is held by the thread in whose proof the hold assertion appears17.

The simplest way to guarantee that the permission hold e R is required to unlock e is to require that all lock invariants R satisfy the relation R = (hold e R)∗S for some additional assertion S. The simplest

way to get this property is via the recursion operator µ:

–  –  –

Because hold e R is always closed and precise, as long as S is closed and precise then (hold e R) ∗ S is as well. In other words, S is tight if and only if (hold e R)∗S is tight. One advantage of this approach is that lock invariants cannot be emp, a fact that is useful when establishing soundness18. See section 4.9.1 for a sample resource invariant created with the recursion µ operator.

Fractional ownership of the hold permission is possible, but does not seem to be very useful.

In fact, an alternative way of getting soundness is to do away with hold altogether, and simply to require that lock invariants be nonempty. The problem with allowing lock invariants to be empty is that it allows a thread to unlock a lock twice.



4.7.3 Functions

We reason about first-class functions with the assertion f : {P }{Q}, which means that the expression f evaluates to a function pointer that points to a function with precondition P and postcondition Q. A precondition P of a function is actually a map from function arguments e to an assertion; similarly, the postcondition Q is a map from the values returned by the function to an assertion19. To allow a function’s pre- and postconditions to be related to each other (e.g., function f returns an integer twice as large as its input), there is also an additional parameter for both P and Q. The ability to relate postconditions to preconditions is not so interesting for spawnable functions since the spawned functions never return to their parent. Therefore in this presentation we elide this extra parameter; see Appel and Blazy [AB07] for a discussion of how it is used for reasoning about sequential function call.

Since C minor separates the “data memory” from the “program memory,” functions do not have shares, and every function is visible to every thread20. A function can either be called (within the current thread) or spawned (as a new thread). We require that the preconditions of functions that will be spawned be precise. We enforce this requirement with the validly and precisely operators analogously to our use of tightly for lock invariants. This way it is simple to determine Our version of C minor supports multiple return values.

If one wished to verify self-modifying code, for example, functions would need shares.


–  –  –

One of the most important aspects of O’Hearn’s CSL is that it includes all of the rules of standard separation logic [O’H07]. Similarily, our CSL rules are a superset of the rules of Appel & Blazy presented in figure

2.6. Our new concurrent rules are presented in figure 4.1.

To use the make lock rule to reason about making a lock with invariant R at location e, full ownership of e is required. Moreover, that location must contain a 0; the operational semantics described in secCHAPTER 4. CONCURRENT SEPARATION LOGIC  tion ?? will get stuck if these conditions are not met. Since a lock is considered to be locked when its location contains a 0, it is therefore created in the locked state, and the postcondition includes both the full ◭◮ visibility of the lock e ; R and the holding of the lock hold e R.

◭◮ Both e ; R and hold e R are required to reason about freeing a lock using the free lock rule. Since a thread can have a hold permission only if the lock is locked, this means that the location associated with the lock contains a 0.

To use the lock rule to reason about locking a lock e with associated invariant R, a thread needs to own some (typically partial) share π of e. After locking, the thread still has the same visibility of the lock as before, and in addition gains the assertion tightly R. If R is tight, then tightly R is equal to R.

The precondition for using the unlock rule for reasoning about unlocking a lock is tightly R. We also require as a side condition that the lock invariant R be equal to (hold e R) ∗ S for some S 21. Again, as long as R is tight (which is true if and only if S is tight) then the precondition is equal to R. If R is not tight, then tightly R is equal to false, meaning that the unlock statement cannot be proven to be safe using CSL.

The rule for fork is somewhat analogous to the rule for unlock. This is natural since in both cases resources are being transferred from the In the Coq development, this property is enforced not by a side condition but instead by using another operator like tightly; the presentation here is equivalent and cleaner.

Pages:     | 1 |   ...   | 5 | 6 || 8 | 9 |   ...   | 22 |

Similar works:

«ABSTRACT DESIGN AND PERFORMANCE PREDICTION Title of dissertation: OF SWASHPLATELESS HELICOPTER ROTOR WITH TRAILING EDGE FLAPS AND TABS Jaye Falls, Doctor of Philosophy, 2010 Professor Inderjit Chopra Dissertation directed by: Department of Aerospace Engineering This work studies the design of trailing edge controls for swashplateless helicopter primary control, and examines the impact of those controls on the performance of the rotor. The objective is to develop a comprehensive aeroelastic...»

«UNIVERSITY OF CALIFORNIA, SAN DIEGO Efficient Thermal Management for Multiprocessor Systems A dissertation submitted in partial satisfaction of the requirements for the degree Doctor of Philosophy in Computer Science and Engineering by Ay¸e Kıvılcım Co¸kun s s Committee in charge: ˘ Tajana Simuni´ Rosing, Chair c Kenny C. Gross Rajesh Gupta Tara Javidi Andrew B. Kahng Dean Tullsen 2009 Copyright Ay¸e Kıvılcım Co¸kun, 2009 s s All rights reserved. The dissertation of Ay¸e...»

«THE ROLE OF ENDOCYTOSIS IN NEURONAL MIGRATION A DISSERTATION SUBMITTED TO THE NEUROSCIENCES PROGRAM AND THE COMMITTEE ON GRADUATE STUDIES OF STANFORD UNIVERSITY IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY Jennifer Cynthia Shieh March 2010 © 2010 by Jennifer Cynthia Shieh. All Rights Reserved. Re-distributed by Stanford University under license with the author. This dissertation is online at: http://purl.stanford.edu/dj352gy7333 Includes supplemental files:...»

«PLANTING DEPTH OF TREES – A SURVEY OF FIELD DEPTH, EFFECT OF DEEP PLANTING AND REMEDIATION DISSERTATION Presented in Partial Fulfillment of the Requirements for the Degree Doctor of Philosophy in the Graduate School of The Ohio State University By Richard G. Rathjens, M. S. The Ohio State University Dissertation Committee: Dr. T. Davis Sydnor, Advisor Approved by Dr. David S. Gardner Dr. Edward L. McCoy Adviser Dr. James D. Metzger Envir. & Natural Resources Graduate Program Dr. Brent...»

«Famous Writers More or Less The Beat Generation as a Literary Coterie by Christopher Graham Challis Thesis Submitted to the Department of English University of Leicester For the degree of Doctor of Philosophy UMI Number: U439544 All rights reserved INFORMATION TO ALL USERS The quality of this reproduction is dependent upon the quality of the copy submitted. In the unlikely event that the author did not send a complete manuscript and there are missing pages, these will be noted. Also, if...»

«The Lamont Harp The Healing Harp (From Druid Tradition) By Susa Morgan Black, FSA, Scot Harper, Druid (OBOD) Quote “Music is the principle that unites body, soul, and spirit.” – Boethius, 6th century philosopher.The Healing Musician, Stella Benson Irish Legends The Daghdha (Dagda) was the Chief Druid and King of the mythical Tuatha Dé Danann – the faerie race of Ireland and Scotland. He played an enchanted harp, called Una, which produced three magical strains of music – Geantraí,...»

«Additional material: WORSHIP: Luke Worship with the Gospels LUKE Background: These resources were first produced by Clare Amos for ‘Partners in Learning’ an ecumenical resource of learning resources for all ages based on the lectionary readings and themes. They have been adapted here as a resource to encourage congregations to bring ‘the particular interests, topics and concerns of each gospel writer’ into our worship. We would be delighted if you want to use and adapt the material for...»

«2nd Circular Greek Philophophical Society (GPS) International Association of Greek Philosophy (IAGP) Philosophical Society of Cyprus (PSC) Editor: Professor Konstantine Boudouris, President of HOC ISBN: 978-960-91844-2-7 World Congress in Philosophy The Philosophy of Aristotle Παγκόσμιο Συνέδριο Φιλοσοφίας Η φιλοσοφία του Αριστοτέλους Ὑπόθεσις δημοκρατικῆς πολιτείας “Ὑπόθεσις μὲν οὖν τῆς...»

«Indian Feminism (1921–1947): Cosmopolitan Visions and the Traffic in Women Tara Suri Murray Edwards College, University of Cambridge Multi-Disciplinary Gender Studies, Department of Geography Word Count: 19,981 July 2014 This dissertation is submitted for the degree of Master of Philosophy. Preface Declaration: This dissertation is the result of my own work and includes nothing which is the outcome of work done in collaboration except where specifically indicated in the text. Statement of...»

«Chapter 2 Estrangement: A Beginner’s Guide to the Strangeness of the World Jonathan M. Smith Abstract Geographers adopted the concept of Being-in-the-World from Martin Heidegger. However, most have wisely eschewed the philosopher’s larger ontological and pantheistic project. Nevertheless, geographers can make use of basic phenomenological concepts and terms. The world of appearances can be reduced to the three basic phenomena of objects, subjects, and death, and each of these phenomena...»

«FRANCES YATES SELECTED WORKS FRANCES YATES Selected Works VOLUME I The valois Tapestries VOLUME II Giordano Bruno and the Hermetic Tradition VOLUME III The Art of Memory VOLUME IV The Rosicrucian Enlightenment VOLUME V Astraea VOLUME VI Shakespeare's Last Plays VOLUME VII The Occult Philosophy in the Elizabethan Age VOLUME VIII Lull and Bruno VOLUME IX Renaissance and Riform: The Italian Contribution VOLUME X Ideas and Ideals in the North European Renaissance FRANCES YATES Selected Works Volume...»

«University of Iowa Iowa Research Online Theses and Dissertations The educational and occupational aspirations of Sudanese refugee youth in an American public high school in the Midwest Anne Omwango Kiche University of Iowa Copyright 2010 Anne Omwango Kiche This dissertation is available at Iowa Research Online: http://ir.uiowa.edu/etd/527 Recommended Citation Kiche, Anne Omwango. The educational and occupational aspirations of Sudanese refugee youth in an American public high school in the...»

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