FREE ELECTRONIC LIBRARY - Dissertations, online materials

Pages:     | 1 |   ...   | 19 | 20 || 22 |

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

-- [ Page 21 ] --

11.1. STATE OF THE COQ DEVELOPMENT  Separation Logic with respect to the concurrent operational semantics of Concurrent C minor.

11.1 State of the Coq Development As we have indicated in the text, the Coq development is incomplete.

The tasks that remain are:

1. Integrate the cleaner definitions for joinable types and shares that were presented in chapter 4.

2. Add the function pool to the concurrent machine state. We are attempting to develop a better solution to the problem of global and immutable data in separation logic, and since the function pool is a bit of a hack we have held off implementing it in Coq until we can study the other alternatives in more detail.

3. Finish the modularization work presented in chapter 6. We have been modularizing the proof incrementally.

4. Do clean-ups as noted in the text.

5. Finish the proof of the CSL unlock rule.

6. Finish the preservation proof.

We developed a slogan when working on the proof, which was “As expected, it took longer than expected.” We also agree with the obserCHAPTER 11. CONCLUSIONS AND FUTURE WORK  vation of Leroy, who noted that “Building [proof] scripts is surprisingly addictive, in a videogame kind of way” [Ler06].

–  –  –

One of the major benefits of the project has been that it has a number

of promising tasks for future work. These include:

1. Modifying the CompCert compiler to handle concurrency. Our plan is to create an oracle semantics for each intermediate language of the compiler by applying our extension and then update the correctness proofs to show that the compiler preserves the behavior of each oracular semantics.

2. Developing techniques to reason about lock-free algorithms of various kinds. In practice, many of the concurrent algorithms used do not use locks, instead relying on various lock-free techniques such as atomic loads and stores. One goal is to see how we can apply our oracle semantics towards reasoning about these kinds of algorithms.

3. Reasoning in the presence of weak memory models. Modern processors execute memory accesses out of program order in a way

–  –  –

4. Exposing implication to end-user by improving dependent/stratified model. Because users of Hoare logics are accustomed to having full implication, it would be useful to be able to improve our assertion models to expose full implication to the CSL user.

5. Developing techniques to better reason about globals and shared immutable data in separation logic. We had a suprisingly difficult time creating global values. We added the function pool to solve this problem, but we want to design a more elegant technique.

11.3 Concluding thoughts We have developed a soundness proof for a powerful new Concurrent Separation Logic with first-class locks and threads. Along the way, we developed a modal substructural logic; designed a new style of concurrent operational semantics that did bookkeeping to guarantee behavior;

designed a new oracle semantics that presented a thread-local view of a concurrent machine and that allowed for the re-use of metaproofs of sequential language features; and provided a new modal definition of the Hoare tuple. Our Coq proofs have been almost completed, giving a high degree of assurance, and are designed to support the modification of the CompCert compiler, thereby supporting the goal of providing an end-to-end guarantee about the behavior of concurrent programs.

Appendix A A Miniature Model in Coq A.1 Headers (* Aquinas Hobor *) Require Import List.

Parameter address : Type.

Parameter value : Type.

Parameter share : Type.

Parameter kind : Type.

Definition memory : Type := address - value.

–  –  –

A.2 Stratified Model Section Stratified_Model.

Inductive res_n’ (inv : Type) : Type :=

| NO’ | YES’: kind - share - (list inv) - res_n’ inv.

Definition rmap_n’ (inv : Type) : Type :=

address - res_n’ inv.

Fixpoint inv_n (n: nat) : Type :=

match n with | O = unit | S n = ((inv_n n) * (rmap_n’ (inv_n n) * memory - Prop))%type end.

Definition res_n (n: nat) : Type :=

res_n’ (inv_n n).

Definition rmap_n (n: nat) : Type :=

rmap_n’ (inv_n n).

–  –  –

A.3 Dependent Model Section Dependent_Model.

Inductive resource’ : Type :=

res_Level : forall (n : nat), res_n n - resource’.

Definition resource := resource’.

Inductive rmap’ : Type :=

rm_Level : forall (n : nat), rmap_n n - rmap’.

Definition rmap := rmap’.

Definition predicate : Type := (rmap * memory) - Prop.

End Dependent_Model.


 A.4 Private definitions relating public to

–  –  –

Section Private_Defs.

Definition level (rm: rmap) : nat :=

match rm with rm_Level n _ = n end.

Fixpoint stratify (n : nat) (P : predicate) : inv_n n :=

match n as n return inv_n n with | O = tt

–  –  –

End Private_Defs.

A.5. PUBLIC INTERFACE TO ACQUIRE RESOURCE  A.5 Public interface to acquire resource Section Public_Interface.

Definition resource_at (rm: rmap) (addr: address) : resource :=

match rm with rm_Level n rm_n = res_Level n (rm_n addr) end.

Definition NO (rm: rmap) : resource :=

res_Level (level rm) (NO’ (inv_n (level rm))).

Definition YES (rm: rmap)

–  –  –

Lemma. The unlock rule of CSL is sound.

Proof. As discussed in section 10.2.3, we first need to show that the precondition of the CSL lock rule guarantees that the concurrent step relation will not be stuck in cases Ω-diverges and Ω-steps. The precondition of the lock rule is tightly R, and in addition we have the fact that R = (hold e R ∗ S). We need to show that these guarantee that we can take a step with the cstep-unlock rule of the concurrent machine. We are guaranteed that we are at the head of the scheduler by the StepOthers relation, which handles the first premise. Since we know tightly R, and R = (hold e R ∗ S), we know tightly (hold e R ∗ S). Since hold is tight, we know hold e R. By the consistency requirements on the concurrent machine state, if this permission is in a thread’s resource

–  –  –

map, the lock must be locked, so m(e) must be equal to 0, which handles the second premise. The third premise, involving the new memory m′ is true by construction. The forth premise, which says that we can split off a world φlock from φ, is always true, although in most cases φlock is not uniquely determined. The sixth premise, which is that we have hold e R, has already been demonstrated. The seventh premise, which is that tightly R holds on the resource map φlock, is guaranteed since it held on the resource map φ. Moreover, since all tight predicates are precise, this guarantees that φlock is unique. The eigth premise, which is that we can add the newly unlocked lock to the lock pool, is true by constrction and because we can prove that it was not in the lock pool before, since due to the consistency requirements lock pools can only hold unlocked locks and prior to this point the lock was locked. The nineth premise, the construction of new thread list, is true by construction. The tenth premise, that we can context switch, is true because as long as we have remaining stratification levels we can context switch, and if we had run out of stratification levels then we would have been immediately safe. Now that we have proved all of the premises to the cstep-unlock rule, we must prove that the new concurrent machine state S’ is consistent. From section 8.4 we must prove six properties. First, we must show that there exists a new total resource map. The lock rule does not add or remove from the total resource map, instead simply

–  –  –

of stratification this is possible to do. Second, we must show that the scheduler is still longer than the remaining stratification; since context switch removes exactly one item from the scheduler and ages the worlds exactly once this is simple. Third, we must prove that if any threads are waiting on a memory location then that location is a lock. Since we have not modified any of the other threads, and are not waiting on a lock ourselves, and have not freed any locks, this is simple. Fourth, we must have a well-formed alloc pool; since we have not changed it this is trivial. Fifth, we must have a well-formed function pool; since we have not changed it this is trivial. Sixth and last, we must show that we still have a well formed lock pool. As discussed, the property P3 behaves correctly as the world ages; since we have not touched any of the other locks in the lock pool, and the consistency requirements on the concurrent machine state ensures that the newly unlocked lock’s memory locations do not overlap with any previously unlocked lock’s memory locations, all of the other locks in the lock pool are still sound. For the lock we are unlocking, we need to show that there exists a lock invariant for it—but this is easy, since we have that as a premise—and that the invariant holds tightly on the lock’s resource map; however this is just premise seven from the cstep-unlock rule. Therefore, we have a consistant machine state and so are able to take a step with the cstep-unlock rule. Now we have to prove the postcondition of the rule. Fortunately

–  –  –

does return control, case Ω-steps, we need only satisfy the postcondition of emp, and since we have given away our precondition by putting it into the lock pool, it is easy to satisfy.

–  –  –

Lemma. The child resulting from the fork is safe-as i.

Proof. By all-funs-spawnable, we know that there exists a Γ which believe can connect to the program Ψ. By the precondition to the cstep-fork rule, we know f : {validly precisely P }{Q} for some precondition P and postcondition Q. Since this implies that rkind(φT @ f ) = Some kFUN, by the second half of all-funs-spawnable we know that there exists some (possibly different) precondition P ′ and postcontcondition Q′ such that f : {P ′ }{Q′ } and Γ ⊂ true ∗ f : {P ′}{Q′ }. By YES inversion we know that ⊲ validly precisely P = ⊲ P ′. By the definition of believe, we know ⊲ Htuple(Γ, P ′, Ψ(f ), Q′). By the precondition to the

–  –  –

rule, we will have P ′ and Htuple(Γ, P ′, Ψ(f ), Q′ ). By the definition of Htuple and since we have believe Htuple Γ Ψ, by fold-unfold we know

–  –  –

By the cstep-fork rule, the child will be started with initial control1 call f · Kstop and an initial world satisfying ⊲ validly precisely P, i.e., P ′. The key action of the call statement is to step from this control to the control Ψ(f ) · Kstop. Since the function pool φfp is passed into each function as it runs, and since the function pool contains all of the functions in Γ, at the time when the thread is running we will know Γ∗P ′. By the definition of pguard, we will thus know psafe Ψ Ψ(f )·Kstop, which means that the child is safe-as i.

We remove the function arguments for simplicity.

Bibliography [AAV02] Amal Ahmed, Andrew W. Appel, and Roberto Virga. A stratified semantics of general references embeddable in higher-order logic. In 17th Annual IEEE Symp. on Logic in Computer Science, pages 75–86, June 2002.

[AAV03] Amal Ahmed, Andrew W. Appel, and Roberto Virga. An indexed model of impredicative polymorphism and mutable references. http://www.cs.princeton.edu/~appel/papers/ impred.pdf, January 2003.

[AB07] Andrew W. Appel and Sandrine Blazy. Separation logic for small-step C minor. In 20th International Conference on Theorem Proving in Higher-Order Logics (TPHOLs 2007), 2007.

[ABF+ 05] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the

–  –  –

[Ahm04] Amal J. Ahmed. Semantics of Types for Mutable State.

PhD thesis, Princeton University, Princeton, NJ, November

2004. Tech Report TR-713-04.

[AM01] Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems, 23(5):657–683, September 2001.

–  –  –

[App01] Andrew W. Appel. Foundational proof-carrying code. In Symp. on Logic in Computer Science (LICS ’01), pages 247–258. IEEE, 2001.

–  –  –

[App08] Andrew W. Appel. A core resource calculus for higher-order separation logics. unpublished manuscript, 2008.

[BCOP05] Richard Bornat, Cristiano Calcagno, Peter O’Hearn, and Matthew Parkinson. Permission accounting in separation logic. In POPL ’05: 32nd ACM Symp. on Principles of Programming Languages, pages 259–270, 2005.

[BDH+ 08] C. J. Bell, Robert Dockins, Aquinas Hobor, Andrew W. Appel, and David Walker. Comparing semantic and syntactic methods in mechanized proof frameworks. In Proceedings of the 2nd International Workshop on Proof-Carrying Code (PCC 2008), 2008.

[Boy03] J. Boyland. Checking interference with fractional permissions. In Static Analysis: 10th International Symposium, pages 55–72, 2003.

[Bro07] Stephen Brookes. A semantics for concurrent separation logic. Theoretical Computer Science, 375(1):227–270, May 2007.

[COY07] Cristiano Calcagno, Peter W. O’Hearn, and Hongseok Yang. Local action and abstract separation logic. In LICS 2007 IEEE Symposium on Logic in Computer Science, 2007.

–  –  –

Pages:     | 1 |   ...   | 19 | 20 || 22 |

Similar works:

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

«Ghrelin The Defender of Fat in the Face of Stress Implications in Obesity Treatment Zachary R. Patterson A thesis submitted to the Faculty of Graduate & Postdoctoral Affairs in partial fulfillment of the requirements of the degree of Doctor of Philosophy in Neuroscience Carleton University Ottawa, ON Copyright © 2013 Zachary R. Patterson ii 0.1 Abstract Chronic activation of the stress response can lead to a number of metabolic disturbances such as obesity, metabolic syndrome, Type II...»

«EFFECT OF TRUST AND RISK ON IT OUTSOURCING RELATIONSHIP QUALITY AND OUTSOURCING SUCCESS A Thesis Submitted to the Faculty of Drexel University by Narasimha Paravastu in partial fulfillment of the requirements for the degree of Doctor of Philosophy January, 2007 ii © Copyright 2007 Narasimha Paravastu. All Rights Reserved. iii DEDICATIONS TO MY GRAND FATHER LATE P.S.S. RAMANUJA SWAMI WITH REVERENCE AND LOVE iv ACKNOWLEDGMENTS I would like to deeply thank many people for helping me during the...»

«LEADING POINTS CONCEPTS IN TURBULENT PREMIXED COMBUSTION MODELING A Dissertation Presented to The Academic Faculty by Alberto Amato In Partial Fulfillment of the Requirements for the Degree Doctor of Philosophy in the School of Mechanical Engineering Georgia Institute of Technology August 2014 Copyright 2014 by Alberto Amato LEADING POINTS CONCEPTS IN TURBULENT PREMIXED COMBUSTION MODELING Approved by: Dr. Tim Lieuwen, Advisor Dr. Yuri Bakhtin School of Aerospace Engineering School of...»


«TAINTED PROOFS: STAGING WRITTEN EVIDENCE IN EARLY MODERN DRAMA By Lisa M. Barksdale-Shaw A DISSERTATION Submitted to Michigan State University in partial fulfillment of the requirements for the degree of English-Doctor of Philosophy 2015 ABSTRACT TAINTED PROOFS: STAGING WRITTEN EVIDENCE IN EARLY MODERN DRAMA By Lisa M. Barksdale-Shaw Tainted Proofs examines how drama presents stage properties, like letters, contracts, and wills, in the early modern theatre. I argue that the playwrights, William...»

«DYNAMIC RESOURCE MANAGEMENT IN RESOURCE-OVERBOOKED CLOUD DATA CENTERS By Faruk Caglar 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 Computer Science August, 2015 Nashville, Tennessee Approved: Dr. Aniruddha S. Gokhale Dr. Douglas C. Schmidt Dr. Gautam Biswas Dr. Christopher J. White Dr. Akos Ledeczi To my beloved wife Fatma for her patience, encouragement, and support...»

«1 Faith and Philosophy, April (2006), 191-200. Penultimate Draft DE SE KNOWLEDGE AND THE POSSIBILITY OF AN OMNISCIENT BEING Stephan Torre In this paper I examine an argument that has been made by Patrick Grim for the claim that de se knowledge is incompatible with the existence of an omniscient being. I claim that the success of the argument depends upon whether it is possible for someone else to know what I know in knowing (F), where (F) is a claim involving de se knowledge. I discuss one...»

«THE DIGITAL AFFECT: A RHETORICAL HERMENEUTIC FOR READING, WRITING, AND UNDERSTANDING NARRATIVE IN CONTEMPORARY LITERATURE AND NEW MEDIA by Richard Elliott Parent II Bachelor of Arts, University of North Texas, 1994 Master of Arts, Mills College, 2000 Submitted to the Graduate Faculty of Arts and Sciences in partial fulfillment of the requirements for the degree of Doctor of Philosophy in English: Cultural and Critical Studies University of Pittsburgh UNIVERSITY OF PITTSBURGH ARTS AND SCIENCES...»

«JACK L. SKINNER, PH.D., P.E. ASSOCIATE PROFESSOR OF MECHANICAL ENGINEERING DEPARTMENT OF GENERAL ENGINEERING MONTANA TECH OF THE UNIVERSITY OF MONTANA 1300 WEST PARK ST. BUTTE, MT 59701 (406) 496-4460 JSKINNER@MTECH.EDU EDUCATION & LICENSING Doctor of Philosophy in Mechanical Engineering (September 2004-December 2007) Dissertation Title: Diffractive Optical MEMS Technology for Tunable Filters and Modulators Advisor: David A. Horsley Major: Dynamics and Control Systems / Microelectromechanical...»

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

«Investigation of Nanostructured Semiconducting Metal Oxide and Conducting Polymer Thin Films for Gas Sensing Applications A thesis submitted in fulfilment of the requirements for the degree of Doctor of Philosophy Abu Zafar Md Sadek B.Sc.Eng. (Electrical and Electronic Engineering), Bangladesh University of Engineering & Technology (BUET), Dhaka, Bangladesh M.Eng. (Telecommunications), The University of Melbourne, Australia School of Electrical and Computer Engineering RMIT University,...»

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