FREE ELECTRONIC LIBRARY - Dissertations, online materials

Pages:     | 1 |   ...   | 2 | 3 || 5 | 6 |   ...   | 22 |

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

-- [ Page 4 ] --

2.2.3 Brookes’s Soundness Result When CSL was developed there were serious doubts about the soundness of the whole approach [O’H]. Reynolds concocted a clever example in which a typical rule of separation logic, the conjunction rule, did not hold [O’H07]. An additional technical requirement on resource invariRELY/GUARANTEE  ants called precision seemed to help, but it was unclear if other troubles were lurking.

Fortunately, Brookes was able to develop a soundness proof for CSL [Bro07], in which he uses a local interpretation of program traces to model the semantics of CSL. Brookes was aided by some of the simplications of CSL, particularlly including the lack of first-class locks and functions, but it was still a very noteworthy development. Although we depart from Brookes’s model in many respects, there are several ideas in common, including the idea of modeling a race condition as a fatal error in the program execution.

2.2.4 Summary of Concurrent Separation Logic As mentioned, there were several limitations and drawbacks to the approach as originally stated. However, the basic idea—that threads usually execute on private data, and communicate via special synchronization primitives such as locks, which control access to shared resources— is both natural and powerful. Moreover, the ability to re-use verification results from sequential separation logic is a powerful advantage.

2.3 Rely/Guarantee The idea of verifying concurrent programs by relying on noninterference was introduced by Owicki and Gries [OG76]. However, their method was not compositional. Jones introduced the rely/guarantee method


 [Jon83], which has a more modular design. Each thread is given a pair of assertions, one of which is the rely for that thread and the other of which is the guarantee. The thread is allowed to assume that the rely always holds, and must never break the invariants of the guarantee. Other threads will then be able to rely on the current thread’s guarantee, and will be responsible themselves for guaranteeing the current thread’s rely.

Rely/guarantee allows for relatively modular reasoning at the thread level, but one major drawback is that the flavor of the rely/guarantee assertions is quite global. However, it is quite good at reasoning about interference between threads. In contrast, concurrent separation logic allows for much more local reasoning, but to reason about thread interference can require large numbers of auxiliary variables and unnatural proofs.

It is natural to hope to combine the two approaches, and Vafeiadis and Parkinson [VP07] demonstrate how to do so. Their combination allows a verification to contain the local reasoning typical of concurrent

–  –  –

The CompCert system was one of the first optimizing compilers to be proved correct with a machine-checked proof [Ler06]. CompCert consists of a definition of the C minor language, a certifying compiler, and that compiler’s correctness proofs.

2.4.1 The C minor language C minor is a simple imperative language based on C. It is intended to be the highest intermediate-level language in a compiler, but is elegant enough that one could write programs directly in C minor (e.g., a garbage collector). C minor contains expressions, statements, functions, and programs, composed in the standard way. The full grammar for the original C minor expressions is given in figure 2.1. Like expressions in C, expressions in C minor can have side effects and can contain function calls. C minor supports the full memory model of ANSI C,



–  –  –

including such features as pointer arithmetic and loading and storing variously-sized data from memory (the chunk parameter specifies data size). Unlike C, C minor requires explicit conversions and does not overload arithmatical operators. C minor expressions also include some features more commonly found in functional languages, such as local variable binding.

The full grammar for the original C minor statements is given in figure 2.2. Since expressions have side effects, most computation is done with a sequence of expressions. Control flow is given by a combination loop, if-else constructs, and block constructs. The exit n statement prematurely terminates the n enclosing block constructs. There is no general goto statement.

As originally presented, C minor was given a big-step structured operational semantics. The semantics was completely deterministic. Expressions evaluate to values v, which can be 32-bit integers, 64-bit floats,

–  –  –

is the final contents of memory, plus a value returned from the special function main. One negative consequence of the choice of big-step semantics is the inability to reason about nonterminating computations and the difficulty in extending the semantics to handle concurrency.

2.4.2 The CompCert system

The CompCert compiler translates C minor into PowerPC assembly code. The translation is via several intermediate languages, with numerous optimizations and transformations, e.g. constant propagation, common subexpression elimination, register allocation, etc. Generally speaking, performance of compiled code is adequate, and compilation time is reasonable.

What was novel about the CompCert compiler, however, was that the system includes a proof of correctness, stating that the compiled code was a faithful translation of the source code. In other words, the compiler has no bugs that compromise correctness of the generated code3.

The compiler itself is only about 13% of the total code. The remaining code is the proof of correctness. This includes (1) the specification of compiler correctness, including the formal syntax and semantics of C minor and the PowerPC (8%), (2) statements of intermediate theorems, supporting lemmas, and associated definitions (22%), (3) proof scripts for generating the proofs (50%), and (4) custom tactics for the proof Unlike for correctness, there is no formal guarantee of the performance of the generated code. However, in tests CompCert code was competitive with gcc -O1.


 scripts (7%). Note that the Trusted Computing Base of the system (1) is thus slightly over half of the size of the compiler itself. However, as the compiler becomes more complicated, for example by introducing new optimizations, the specification of the system should not grow significantly.

Still, there is an interesting observation to be made: the specification and proofs of correctness of the compiler were approximately eight times larger than the implementation of the compiler. Beyond illustrating the the importance of good proof engineering, it is clear that when one wishes to modify the CompCert compiler, it is very important to consider the effects the change will have on the associated proofs.

This reality means that some changes can be much easier to make than others, even if both require roughly the same amount of modification to the compiler. This is particuarlly noticable for those kinds of changes that break invariants assumed by the correctness proofs.

One shortcoming of the CompCert system is that it is not obvious how to extend it to handle concurrency. In fact, the extension to concurrency is exactly the kind of extension that is so difficult, since the concurrency breaks many of the assumptions used by the proof. Ironically, changing the compiler itself to handle concurrency is probably fairly simple4 – almost all of the difficulty is expected to be in modifying the proof of correctness.

Changing the compiler is relatively simple because although CompCert is an optimizing compiler it does not do the kinds of aggressive optimizations that would be unsound in a concurrent setting, and can simply compile purely concurrent instructions like lock as if they were function calls to an external library.


2.5 Separation Logic for C minor Another issue with the CompCert system is that while the system does guarantee that the target code has the same behavior as the source code, it does not provide an easy way to determine exactly what the behavior of the source code is. As mentioned above, the CompCert compiler is specified and proven correct with respect to the operational semantics of C minor and PowerPC. However, when verifying concrete source programs, it is usually simpler to use some kind of axiomatic semantics, such as sequential separation logic.

This was the major problem that Appel and Blazy [AB07] solved when they defined a separation logic for C minor, and proved it sound in Coq. As a key part of that work, they made many modifications to the C minor language and its semantics to better support the separation logic and future developments involving the C minor universe. The key changes to C minor developed by Appel and Blazy, in consultation with

Leroy, are:

1. Modifying C minor to be more machine-independent

2. Modifying C minor to be a better target language for ML and Object Oriented languages

3. Changing the operational semantics from big-step to small-step

–  –  –

The first two changes substantially enhanse the ability of C minor and CompCert to be used more broadly, connecting more source languages to more target machines. This is quite important for the system as a whole, but it is the second two changes that are of primary concern to people who wish to add concurrency to the CompCert system.

2.5.1 A small-step relation for C minor The third change, moving from a big-step semantics to a small-step one, is obviously useful for reasoning about concurrency. With only a bigstep semantics, it is impossible to reason about partial computations, and the key point about concurrent computation is that communication between interacting threads always happens at midway points in the computation.

–  –  –

where, σ is a state and κ is a control. A state σ in Appel and Blazy’s

C minor is a tuple σ = (Ψ, sp, ρ, φ, m), where:

• Ψ is a pair of program (mapping of addresses to function bodies) and global variable bindings (mapping of identifiers to addresses)

–  –  –

• φ is a new component added by Appel and Blazy, the footprint, which is a mapping from addresses to permissions, explained below

• m is the memory (mapping from addresses to values) A control κ is a stack of the current instructions to be executed, block exit points, and function return points. Using their small-step relation, Appel and Blazy define safe(σ, κ) in the usual way – that the continuation (σ, κ) will never get stuck5.

As is common in formal methods, when a program enters an error state or has undefined behavior we say that the program “gets stuck”. The major goal of a safety proof is to guarantee that programs do not get stuck.

Σ indicates which parameters are integers and which are floating-point, and helps the compiler allocate registers for function calls properly.


 The fourth change, modifying the semantics to better match a clean separation logic, involved many changes; a grammer of the new language is given in figure 2.3. Some, such as changing expressions to be side-effect free, are relatively simple, but simplify reasoning by making side-effects more explicit. A much more complex change was the addition to the semantics of a new component, the footprint.

2.5.2 Footprints, introduced As presented by Appel and Blazy, a footprint φ is a map from memory addresses to permissions. Memory access outside the footprint causes the semantics to get stuck. The simplest model for permissions is a boolean value, with true representing an address which is safe to access and false representing an address which is not. Footprints also come with a join operation, which states which permissions are compatible.

The join operation on footprints is a kind of separation algebra, as explained in section 4.4. The existence of footprints in the semantics became quite important when developing the semantics of Concurrent C minor.

2.5.3 Separation logic for C minor In addition to the changes to the C minor language and semantics, Appel and Blazy designed a separation logic that could handle the control flow and other complex features of C minor. Assertions in separation


–  –  –

Prop, here, is the Coq-level proposition7. One major advantage of defining assertions this way is that one can develop a shallow embedding, which means that when reasoning about the assertions in the Coq theorem prover, one is able to use standard Coq tactics, greatly saving engineering effort. Appel and Blazy define the standard operators of separation logic, as well as several operators more specific to C minor, as given in figure 2.4.

To handle function calls, global variables, function return, and breaking out of multi-level block statements, the Hoare triple is augmented with additional parameters Γ (for globals and functions), R (for the assertion that must be satisfied on function return, and which is a function from the results of the function to assert), and B, a list of the assertions that must be satisfied to exit out of various levels of blocks (a function from the naturals to assert). Therefore, the Hoare judgement

for C minor has the following form:

Γ; R; B ⊢ {P } c {Q} As elegant as this definition is, there is one unfortunate problem with it: since assertions are predicated on states, and states include Ψ, and Ψ includes a function whose range is code (syntax), it is impossible to embed these assertions directly in program syntax. For sequential C minor this was only modestly limiting (for example, it prevents defining an assert statement that takes a real semantic assertion), but when concurrency was added this caused some severe difficulties. In chapter 10 we will show how to solve this problem.


–  –  –

Pages:     | 1 |   ...   | 2 | 3 || 5 | 6 |   ...   | 22 |

Similar works:

«HOW TO TEACH SO THAT PEOPLE LEARN POSTCARDS FROM CORINTH • CHAPTER EXCERPT Postcards is the Users Guide for personal discipleship. While The Compass provides content for one-on-one discipleship, Postcards tackles the practice, philosophy, and difficult challenges that are a part of discipleship. Here, for example, is a partial list of the topics covered: Habitual Sin, Authority Issues, Christian Counseling, Fasting, Theological Conflicts, Coaching Through Trials, Challenging to Conferences,...»

«Behavioral Correlates of Hippocampal Neural Sequences Anoopum S. Gupta CMU-RI-TR-11-36 Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy in Robotics The Robotics Institute School of Computer Science Carnegie Mellon University Pittsburgh, Pennsylvania 15213 September 2011 Thesis Committee David S. Touretzky (Chair) Tai Sing Lee Reid Simmons George Stetten A. David Redish, University of Minnesota Copyright c 2011 by Anoopum S. Gupta. All rights reserved....»

«Droplet impact and spreading of viscous dispersions and volatile solutions Daniel A. Bolleddula A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy University of Washington Program Authorized to Offer Degree: Mechanical Engineering University of Washington Graduate School This is to certify that I have examined this copy of a doctoral dissertation by Daniel A. Bolleddula and have found that it is complete and satisfactory in all respects,...»

«ABSTRACT Title of Dissertation: MULTI-CHANNEL SCANNING SQUID MICROSCOPY Su-Young Lee, Doctor of Philosophy, 2004 Dissertation directed by: Professor Frederick C. Wellstood Department of Physics I designed, fabricated, assembled, and tested an 8-channel high-Tc scanning SQUID system. I started by modifying an existing single-channel 77 K high-Tc scanning SQUID microscope into a multi-channel system with the goal of reducing the scanning time and improving the spatial resolution by increasing the...»

«ABSTRACT QUANTUM SIMULATION OF Title of dissertation: INTERACTING SPIN MODELS WITH TRAPPED IONS Kazi Rajibul Islam, Doctor of Philosophy, 2012 Professor Christopher Monroe Dissertation directed by: Joint Quantum Institute, University of Maryland Department of Physics and National Institute of Standards and Technology The quantum simulation of complex many body systems holds promise for understanding the origin of emergent properties of strongly correlated systems, such as high-Tc...»


«Harmony and Melody as Imitation of Nature in Rameau and Rousseau (Sketch of the oral presentation) José Oscar Marques de Almeida Marques Department of Philosophy State University of Campinas ABSTRACT: Jean-Jacques Rousseau and Jean-Philippe Rameau, the two emblematic figures of the Querelle des Bouffons, could very well agree that music is an imitative art, but what it imitates, nature, was understood by them in very different ways. While Rameau identified nature with the Galilean/Cartesian...»

«SCOPE PARALLELISM AND THE RESOLUTION OF ELLIPSIS AT THE SYNTAX/SEMANTICS INTERFACE Gun ERRE ZREXACH JAVIER In this paper several scope asymmetries in VP ellipsis constructions in English and Spanish are studied. It is argued that an approach based on Fox' (1995 a,b) Ellipsis Scope Generalization faces numerous conceptual and empirical problems. Ellipsis resolution is conceived of as a phenomenon belonging to the conceptual-intentional pan of the computational system that is conditioned by the...»

«1 Against Plantinga's A/C Model: Consequences of the Codependence of the De Jure and De Facto Questions Rebeka Ferreira San Francisco State University 1600 Holloway Avenue Philosophy Department San Francisco, California 94132 rebekadferreira@gmail.com Abstract: Alvin Plantinga's tasks include illustrating that there is no objection to the rationality of theistic belief that does not presuppose theism's falsity, and that it is epistemically possible that theistic belief have warrant in a basic...»

«NORTHWESTERN UNIVERSITY Toward Rotational Cooling of Trapped SiO+ by Optical Pumping A DISSERTATION SUBMITTED TO THE GRADUATE SCHOOL IN PARTIAL FULFILLMENT OF THE REQUIREMENTS for the degree DOCTOR OF PHILOSOPHY Field of Physics and Astronomy By David Tabor EVANSTON, ILLINOIS June 2014 UMI Number: 3627205 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...»

«HARDWARE SIMULATION OF FUEL CELL / GAS TURBINE HYBRIDS A Dissertation Presented to The Academic Faculty By Thomas Paul Smith In Partial Fulfillment Of the Requirements for the Degree Doctor of Philosophy in the School of Mechanical Engineering Georgia Institute of Technology May 2007 Copyright © 2007 by Thomas P. Smith HARDWARE SIMULATION OF FUEL CELL / GAS TURBINE HYBRIDS Approved by: Dr. William J. Wepfer, Co-Advisor Dr. Samuel Graham Woodruff School of Woodruff School of Mechanical...»

«The Hydrologic Evolution of Glacial Meltwater: Insights and Implications from Alpine and Arctic Glaciers by Carli Anne Arendt A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Earth and Environmental Sciences) in the University of Michigan Doctoral Committee: Assistant Professor Sarah M. Aciego, Chair Assistant Professor Jeremy N. Bassis Professor M. Clara Castro Associate Professor Eric A. Hetland Professor Kyger C. Lohmann...»

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