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



Pages:     | 1 |   ...   | 7 | 8 || 10 | 11 |   ...   | 22 |

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

-- [ Page 9 ] --

We denote a thread list by θ, and the ith thread by θi. A concurrent state S is a tuple of schedule ℧, thread list θ, and memory m.

In figure 5.2 we present our erased concurrent step relation with seven cases.

The first case, er-cstep-seq, covers running a sequential statement (including make lock and free lock). We select thread i, add the memory m, and run the sequential step relation; afterwards we put the thread back into place with new locals ρ′ and control κ′ and continue stepping with new memory m′. We do not change the schedule, and so do not context switch.

–  –  –

Figure 5.2: Erased concurrent step relation

CHAPTER 5.

ERASED CONCURRENT OPERATIONAL

SEMANTICS  out of statements in a thread; in this case we switch to another thread by removing the head of the scheduler. We do not delete thread θi from θ, so threads never change position in line. If the thread is selected again, we will just context switch again.

The third case, er-cstep-prelock, covers what happens when a thread wants to start grabbing a lock. We move to the Klock v ctl state and context switch so that other threads have a chance to grab the lock.

The fourth case, er-cstep-nolock, covers the “spin” case of the spin lock. In the memory m lock value is 0, indicating that the lock is locked by some other thread. We context switch and keep waiting for the lock.

The fifth case, er-step-lock, covers the case when we grab the lock.

In the memory m the lock has value 1, indicating that it is unlocked, and so we switch it to value 0, so that no other thread can grab the lock. At a lower level of the compiler this will become a test-and-set or compare-and-swap instruction, making the load from m and the store to m′ atomic at all intermediate compiler levels. We then transition to the runnable Krun κ state and start running the thread.

The sixth case, er-step-unlock, covers the case when we release a lock. In the memory m we test to make sure that the lock is currently locked, and then update it so that it is unlocked. We context switch after an unlock so that other threads can tell that we have released it.

The seventh case, er-step-fork, covers the case when we fork a child thread. In that case we add the new thread to the thread list and context switch so that it has a chance to run.

5.3. REASONABLENESS OF INTERLEAVING MODEL 

5.3 Reasonableness of interleaving model Our semantics has a nonpreemptive thread model. We chose this concurrency model because a sequentially consistent interleaving model is inappropriate for our context.

Sequentially consistent interleaving is too weak because actual processors go beyond interleaving at every step. They have weak memory models, where instructions are dynamically reordered by the processor in a way that is sequentially undetectable. Unfortunately, in the context of concurrency, the weak memory models can change the behavior of a program and thereby cause particularly wicked bugs.

On the other hand, sequentially consistent interleaving models make us do more work than required. The key is that we are not considering all programs, but only programs that are data-race free, i.e., wellsynchronized and verifiable in CSL. For well-synchronized programs interleaving only at concurrent instructions is equivalent to full interleaving; this was the key idea behind Dijkstra’s invention of semaphores.

In fact, we interleave the minimum number of times that preserves the semantics of a full-interleaving semantics. For example, in case er-stepprelock, we context switch even if the lock was already unlocked to let the other threads have a chance to grab it.

In future work we plan to extend our proofs to cover weak memory models. However, it is a mistake to prove that code at the C minor level obeys weak memory models. Instead, we will preserve our “rarely interleaving” semantics all the way through the compiler until we reach

CHAPTER 5. ERASED CONCURRENT OPERATIONAL

SEMANTICS  machine code; only then will we prove the correctness of our semantics for well-synchronized programs executing on a machine with a weak memory model.

5.4 Conclusion In chapter 3 we introduced Concurrent C minor. Here we gave Concurrent C minor a formal erased concurrent operational semantics. Our erased semantics is a reasonable model for conventional concurrency.

It is not easy to prove properties about our erased semantics. It is easier to reason about the unerased semantics defined in chapter 8. In section 8.6 we prove an erasure theorem that says that the unerased semantics is a conservative approximation to the erased semantics given here. In chapter 9 we define an oracular semantics that is suitable for reasoning about one thread at a time. In chapter 10 we model our CSL on that oracular semantics, and prove that properties proved with the oracular semantics hold on the unerased concurrent operational semantics. The erasure theorem then guarantees that the properties hold on our erased semantics.

Chapter 6 Engineering Isolation In chapter 3 we presented the Concurrent C minor language and gave an example program in 3.2. Then in chapter 4 we developed a new concurrent separation logic and demonstrated its power by using it to verify an example program.





In the remainder of this thesis we will present a soundness proof of our Concurrent Separation Logic with respect to the operational semantics of Concurrent C minor. Since the soundness proof is developed in Coq it has aspects of both a mathematical proof and also an engineered software artifact. These aspects have influenced each other: part of the difficulty in developing the mathematical ideas was that they had to integrate cleanly into existing Coq proofs; conversely, at times the engineering process became too difficult and new mathematical techniques had to be developed to simplify the engineering task.

In this chapter, we focus particularly on engineering design choices

–  –  –

that allow for greater modularity in the mechanized Coq proof1. The material in this chapter has not been fully integrated into our Coq development, which uses a somewhat less modular design; work is ongoing to bring the Coq development into closer agreement. In chapter 7, we will develop the modal substructural logic underlying CSL assertions.

In chapter 8 we will explain the operational semantics of Concurrent C minor. In chapter 9 we will introduce the oracle semantics for Concurrent C minor. Finally, in chapter 10, we will construct a modular proof of the soundness of Concurrent Separation Logic using the oracle semantics.

Note to readers uninterested in engineering a large proof in Coq. Readers who are largely uninterested in or unfamiliar with Coq engineering efforts should read section 6.1, and then may skip this chapter until section 6.6, where we define the notation and briefly cover the ideas we will use in the rest of the thesis.

–  –  –

Modules are an engineering technique that isolate parts of a software system from each other. By dividing up the system into isolated components, it becomes easier to understand, maintain, upgrade, and re-use.

In our work, we use modules to isolate the sequential and concurrent parts of the system from each other. In general, reasoning about sequential features or concurrent features is complicated enough; to reason This chapter has not been previously published.

6.1. MODULARIZATION GOALS  about both simultaneously would be very difficult. Also, if our isolation is strong enough, it will be easier to modify the CompCert compiler to compile Concurrent C minor since the existing sequential proofs will not have to be changed very much.

6.1.1 Core, glue, and extension

–  –  –

Languages like C minor have many complex features. At the level of syntax, adding new features is generally done by directly adding new statements into the set of statements already in the language. However, this is not very modular, as many proofs are done using case analysis, and all such proofs must be redone when new statements are added.

Moreover, the semantics of the new language cannot be directly built from the semantics of the old language.

Instead of directly mixing features, we design a “glue” interface layer that allows a core language to be extended with new features.

The glue combines the syntax and semantics of the core and extension to build a new language. The relationship between the core, glue, and extension is illustrated in figure 6.1. Since the glue isolates the core and extension from each other, the glue allows us to re-use proofs about the component parts as lemmas in proofs about the combined language.

CHAPTER 6. ENGINEERING ISOLATION



–  –  –

We will take as the core the C minor of Appel and Blazy [AB07] and as the extension a semantics of the concurrent statements make lock, free lock, lock, unlock, and fork. We glue these together to make Concurrent C minor.

6.1.2 Level independence A major goal of our Concurrent C minor project is to extend the correctness proofs of the CompCert compiler [Ler06] from the sequential

–  –  –

trated in table 6.1. From the source language of C minor to the target language of PowerPC, each sequential language is attached to some semantics of concurrency specialized to that language with its own language-dependent glue.

While this method would work, it would require much more substantial modifications to the CompCert compiler and correctness proofs than ideal, since the reasoning about the statements would have to be done differently for each intermediate language. This would also mean that a change to the new statements would require changing all of the proofs about the intermediate languages. One question is how well the glue isolates the core and extension from each other, and also how much the glue depends on the two of them.

Ideally, the core and extension could be so isolated from each other that each language could use the same extension to add new behavior, as illustrated in table 6.2. To do this, the new statements must fit uniformly into all of the intermediate languages of the CompCert compiler.

While this does make the initial engineering work harder, the benefit should be a substantially easier time modifying the compiler to handle new extensions2.

Since the compiler has not yet been modified, it is quite likely that some additional engineering work beyond what is presented in this chapter will be necessary for that process. In particular, there are concerns that the “oracle” used to build the concurrency extension is not fully level independent. Hopefully, however, this material will provide a good start in the proper direction.

CHAPTER 6. ENGINEERING ISOLATION



–  –  –

We now present an extension system which takes a “core” small-step semantics and extends with certain additional instructions. We will then use this extensible semantics to build Concurrent C minor on top of the C minor of Appel and Blazy[AB07], and then later use it again build an oracular semantics for Concurrent C minor.

6.2.1 Basic definitions All of the languages of the CompCert compiler share certain common definitions, including those given in figure 6.23.

Coq code shown in this chapter has been simplified for the presentation.

6.2. SHARED DEFINITIONS FOR GLUE  1 (* Definitions shared in all CompCert languages *) 3 (* Memory addresses *) 4 Definition addr := Z * Z 6 (* Identifiers *) 7 Definition ident := nat.

9 (* Values *) 10 Inductive val := 11 | Vundef: val 12 | Vint: int - val 13 | Vfloat: float - val 14 | Vptr: addr - val.

16 Definition globals := ident - option addr.

18 Definition locals := ident - option val.

20 (* Lines 21 - 53 are explained in section 5.2.2 *) 21 (* Permissions *) 22 Parameter resource : Type.

24 (* A map from address to permissions *) 25 Parameter rmap : Type.

26-53 (see figure 5.5) 55 Definition mem := address - val.

57 Definition world := 58 globals * locals * rmap * mem.

59 Definition predicate := world - Prop.

61 Definition ext_fun := ident.

Figure 6.2: Shared definitions in all CompCert languages

CHAPTER 6.

ENGINEERING ISOLATION

 Addresses are pairs of integers, which give a block and offset; this allows for greater modularity in the compiler. Identifiers (names of variables) are natural numbers. There are four kinds of values: int, float, pointer, and undefined4. A mapping from identifiers to addresses allows global variables to be used.

Locals. Local variables are tricky to handle uniformly, since each CompCert language has its own representation. To allow reasoning to operate more smoothly with the languages at each level in the compiler, we define a level-independent definition of locals as a map from N to value. Then, each language’s glue will be responsible for converting its own private representation of local variables into the shared one when required.

Resource map. A resource map is a generalization of the footprint defined by Appel and Blazy [AB07]. Recall from section 2.5.2 that a footprint is a map from addresses to permissions. For Appel and Blazy, a permission was simply a binary value, where true meant that memory access to that address was allowed and false meant that memory access was forbidden. In our setting, resource maps and permissions are more complex and are explained in section 6.2.2. Like the rest of the shared definitions, the model of resource maps does not depend on any particular program syntax, meaning that every language in CompCert can use the same definition.

–  –  –

that the same memory model is used for the source, target, and all intermediate languages. For this presentation we simplify the CompCert memory model so that memory is a map from addresses to values;

Leroy et al. [LB08, Ler06] explain the CompCert memory model in more detail.



Pages:     | 1 |   ...   | 7 | 8 || 10 | 11 |   ...   | 22 |


Similar works:

«VIDEO-BASED ANALYSIS OF MATHEMATICS CLASSROOM PRACTICE: EXAMPLES FROM FINLAND AND ICELAND by Lasse Tuomas Savola Dissertation committee: Professor Bruce Vogeli, Sponsor Professor Herbert Ginsburg Professor Robert McClintock Professor O. Roger Anderson Professor Patrick Gallagher Submitted in partial fulfillment of the requirements for the Degree of Doctor of Philosophy under the Executive Committee of The Graduate School of Arts and Sciences Columbia University 2008 © 2008 LASSE TUOMAS SAVOLA...»

«QUANTUM TUNNELING OF ATOMS IN AN OPTICAL POTENTIAL APPROVED BY DISSERTATION COMMITTEE: Supervisor: Copyright by Patrick Russell Morrow 1996 This dissertation is dedicated to my loving wife Xiaorong QUANTUM TUNNELING OF ATOMS IN AN OPTICAL POTENTIAL by PATRICK RUSSELL MORROW, B.S.,B.A. DISSERTATION Presented to the Faculty of the Graduate School of The University of Texas at Austin in Partial Fulfillment of the Requirements for the Degree of DOCTOR OF PHILOSOPHY THE UNIVERSITY OF TEXAS AT...»

«Information Hazards: A Typology of Potential Harms from Knowledge Nick Bostrom Faculty of Philosophy & Oxford Martin School Oxford University [Published in Review of Contemporary Philosophy, Vol. 10 (2011): pp. 44-79] www.nickbostrom.com Abstract Information hazards are risks that arise from the dissemination or the potential dissemination of true information that may cause harm or enable some agent to cause harm. Such hazards are often subtler than direct physical threats, and, as a...»

«AMARA AIT AISSA ETUDE EXPERIMENTALE DE MELANGE DE POUDRES DE POLYMÈRES DANS UN MÉLANGEUR ROTATIF Thèse présentée à la Faculté des études supérieures de l'Université Laval dans le cadre du programme de doctorat en Génie Chimique pour l'obtention du grade de Philosophiae Doctor (PhD) DEPARTEMENT DE GENIE CHIMIQUE FACULTÉ DES SCIENCES ET DE GÉNIE UNIVERSITÉ LAVAL QUÉBEC Amara Ait Aissa, 2011 Résumé Dans ce travail, on développe plusieurs méthodes de mesure en ligne et...»

«Self-Reliance: Ethnography of Literature Outside Viet Nam Daniel Edward Duffy A dissertation submitted to the faculty of the University of North Carolina at Chapel Hill in partial fulfillment of the requirements for the degree of Doctor of Philosophy in the Department of Anthropology. Chapel Hill Approved by James Peacock Carole Crumley Patricia Sawin Eric Henry John McGowan   © 2008 Daniel Edward Duffy ALL RIGHTS RESERVED ii   ABSTRACT DANIEL EDWARD DUFFY: Self Reliance: Ethnography of...»

«POLITECHNIKA GDAŃSKA WYDAJNOŚĆ WARSTWY DRUGIEJ STOSU PROTOKOŁÓW INTERFEJSU RADIOWEGO W SYSTEMIE UMTS mgr in. Paweł Matusz ROZPRAWA DOKTORSKA promotor: prof. dr hab. in. Józef Woźniak WYDZIAŁ ELEKTRONIKI, TELEKOMUNIKACJI I INFORMATYKI GDAŃSK 2005 GDAŃSK UNIVERSITY OF TECHNOLOGY ON EFFICIENCY OF LAYER 2 OF THE RADIO INTERFACE PROTOCOL STACK IN UMTS by Paweł Matusz A dissertation submitted in partial fulfillment of the requirements for the degree of DOCTOR OF PHILOSOPHY supervisor:...»

«1 The Hendrick Hudson Lincoln-Douglas Philosophical Handbook• Version 4.0 (including a few Frenchmen) The HHLDPH (pronounced hull-duff, or Hillary Duff, depending on your native language) is not meant as a substitute for reading the primary materials, but it does sum up much of the information in readable (sort of) bite-sized pieces. The HHLDPH is divided into six parts. They are, in order, Rights, the Social Contract, Justice, Morality, Random Principles/Arguments, and Philosophers. Read...»

«Variation in Child Maltreatment across Wisconsin: The Impact of Prevention Program Service Array By Kathryn Maguire-Jack A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Social Welfare) at the UNIVERSITY OF WISCONSIN-MADISON Date of final oral examination: 04/24/2013 The dissertation is approved by the following members of the Final Oral Committee: Kristen Shook Slack, Director and Professor, Social Work Lawrence Berger, Associate...»

«UNIVERSITY OF CALIFORNIA, IRVINE Evolution of Cooperation: Comparative Study of Kinship Behavior DISSERTATION submitted in partial satisfaction of the requirements for the degree of DOCTOR OF PHILOSOPHY in Mathematical Behavioral Science by ¨ Bahattin Tolga Oztan Dissertation Committee: Professor Douglas R. White, Chair Professor Cailin O’Connor Professor Louis Narens 2016 ¨ c 2016 Bahattin Tolga Oztan DEDICATION To Mom, Dad and Noyan Kalyoncu ii TABLE OF CONTENTS Page LIST OF FIGURES v...»

«Abstract Title of Dissertation: Novel Extracellular Signal-Regulated Kinase (ERK) Targeted Inhibitors Effects on Apoptotic Signaling: A Potential Cancer Therapy Sarice R. Boston, Doctor of Philosophy, 2011 Dissertation directed by: Paul Shapiro, Ph.D. Associate Professor Associate Dean for Research and Graduate Education Department of Pharmaceutical Sciences University of Maryland, Baltimore The extracellular signal-regulated kinase 1 and 2 (ERK 1/2) proteins potently mediate cell proliferation...»

«THERMODYNAMIC STUDIES ON ALTERNATE BINARY WORKING FLUID COMBINATIONS AND CONFIGURATIONS FOR A COMBINED POWER AND COOLING CYCLE By SANJAY VIJAYARAGHAVAN 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 2003 ACKNOWLEDGMENTS The work presented in this dissertation was completed with the encouragement and support of many wonderful people. Working with Dr. Yogi Goswami...»

«STRUCTURE AND PROPERTIES OF ELECTRODEPOSITED NANOCRYSTALLINE NI AND NI-FE ALLOY CONTINUOUS FOILS by Jason Derek Giallonardo A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Department of Materials Science and Engineering University of Toronto © Copyright by Jason Derek Giallonardo (2013) STRUCTURE AND PROPERTIES OF ELECTRODEPOSITED NANOCRYSTALLINE NI AND NI-FE ALLOY CONTINOUS FOILS Jason Derek Giallonardo Doctor of Philosophy Materials Science and...»





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