Modern proof assistants such as Coq and Isabelle provide high degrees of expressiveness and assurance because they support formal reasoning in higher-order logic and supply explicit machine-checkable proof objects. Un...
详细信息
ISBN:
(纸本)9781605587943
Modern proof assistants such as Coq and Isabelle provide high degrees of expressiveness and assurance because they support formal reasoning in higher-order logic and supply explicit machine-checkable proof objects. Unfortunately, large scale proof development in these proof assistants is still an extremely difficult and time-consuming task. One major weakness of these proof assistants is the lack of a single language where users can develop complex tactics and decision procedures using a rich programming model and in a typeful manner. this limits the scalability of the proof development process, as users avoid developing domain-specific tactics and decision procedures. In this paper, we present VeriML-a novel languagedesignthat couples a type-safe effectful computational language with first-class support for manipulating logical terms such as propositions and proofs. the main idea behind our design is to integrate a rich logical framework-similar to the one supported by Coq-inside a computational language inspired by ML. the languagedesign is such that the added features are orthogonal to the rest of the computational language, and also do not require significant additions to the logic language, so soundness is guaranteed. We have built a prototype implementation of VeriML including both its type-checker and an interpreter. We demonstrate the effectiveness of our design by showing a number of type-safe tactics and decision procedures written in VeriML.
the availability of multicore processors has led to significant interest in compiler techniques for speculative parallelization of sequential programs. Isolation of speculative state from non-speculative state forms t...
详细信息
ISBN:
(纸本)9781450300193
the availability of multicore processors has led to significant interest in compiler techniques for speculative parallelization of sequential programs. Isolation of speculative state from non-speculative state forms the basis of such speculative techniques as this separation enables recovery from misspeculations. In our prior work on CorD [35, 36] we showed that for array and scalar variable based programs copying of data between speculative and non-speculative memory can be highly optimized to support state separation that yields significant speedups on multicore machines available today. However, we observe that in context of heap-intensive programs that operate on linked dynamic data structures, state separation based speculative parallelization poses many challenges. the copying of data structures from non-speculative to speculative state (copy-in operation) can be very expensive due to the large sizes of dynamic data structures. the copying of updated data structures from speculative state to non-speculative state (copy-out operation) is made complex due to the changes in the shape and size of the dynamic data structure made by the speculative computation. In addition, we must contend withthe need to translate pointers internal to dynamic data structures between their non-speculative and speculative memory addresses. In this paper we develop an augmented design for the representation of dynamic data structures such that all of the above operations can be performed efficiently. Our experiments demonstrate significant speedups on a real machine for a set of programs that make extensive use of heap based dynamic data structures.
Cody, Hazel, and theo, two experienced Haskell programmers and an expert in automata theory, develop an elegant Haskell program for matching regular expressions: (i) the program is purely functional;(ii) it is overloa...
详细信息
ISBN:
(纸本)9781605587943
Cody, Hazel, and theo, two experienced Haskell programmers and an expert in automata theory, develop an elegant Haskell program for matching regular expressions: (i) the program is purely functional;(ii) it is overloaded over arbitrary semirings, which not only allows to solve the ordinary matching problem but also supports other applications like computing leftmost longest matchings or the number of matchings, all with a single algorithm;(iii) it is more powerful than other matchers, as it can be used for parsing every context-free language by taking advantage of laziness. the developed program is based on an old technique to turn regular expressions into finite automata which makes it efficient both in terms of worst-case time and space bounds and actual performance: despite its simplicity, the Haskell implementation can compete with a recently published professional C++ program for the same problem.
Functional programming presents several important advantages in the design, analysis and implementation of parallel algorithms: It discourages iteration and encourages *** supports persistence and hence easy *** encou...
详细信息
ISBN:
(纸本)9781605587943
Functional programming presents several important advantages in the design, analysis and implementation of parallel algorithms: It discourages iteration and encourages *** supports persistence and hence easy *** encourages higher-order aggregate *** is well suited for defining cost models tied to the programminglanguage rather than the *** can avoid false *** can use cheaper weak consistency *** most importantly, it supports safe deterministic *** fact functional programming supports a level of abstraction in which parallel algorithms are often as easy to design and analyze as sequential algorithms. the recent widespread advent of parallel machines therefore presents a great opportunity for functional programminglanguages. However, any changes will require significant education at all levels and involvement of the functional programming *** this talk I will discuss an approach to designing and analyzing parallel algorithms in a strict functional and fully deterministic setting. Key ideas include a cost model defined in term of analyzing work and span, the use of divide-and-conquer and contraction, the need for arrays (immutable) to achieve asymptotic efficiency, and the power of (deterministic) randomized algorithms. these are all ideas I believe can be taught at any level.
We report on our experience using Haskell as an executable specification language in the formal verification of the seL4 microkernel. the verification connects an abstract operational specification in the theorem prov...
详细信息
ISBN:
(纸本)9781605583327
We report on our experience using Haskell as an executable specification language in the formal verification of the seL4 microkernel. the verification connects an abstract operational specification in the theorem prover Isabelle/HOL to a C implementation of the microkernel. We describe how this project differs from other efforts, and examine the effect of using Haskell in a large-scale formal verification. the kernel comprises 8,700 lines of C code;the verification more than 150,000 lines of proof script.
PHP is a popular language for server-side applications. In PHP, assignment to variables copies the assigned values, according to its so-called copy-on-assignment semantics. In contrast, a typical PHP implementation us...
详细信息
ISBN:
(纸本)9781605583792
PHP is a popular language for server-side applications. In PHP, assignment to variables copies the assigned values, according to its so-called copy-on-assignment semantics. In contrast, a typical PHP implementation uses a copy-on-write scheme to reduce the copy overhead by delaying copies as much as possible. this leads us to ask if the semantics and implementation of PHP coincide, and actually this is not the case in the presence of sharings within values. In this paper, we describe the copy-on-assignment semantics withthree possible strategies to copy values containing sharings. the current PHP implementation has inconsistencies withthese semantics, caused by its naive use of copy-on-write. We fix this problem by the novel mostly copy-on-write scheme, making the copy-on-write implementations faithful to the semantics. We prove that our copy-on-write implementations are correct, using bisimulation withthe copy-on-assignment semantics.
Object versioning refers to how an application can have access to previous states of its objects Implementing this mechanism is hard because it needs to be efficient in space and time, and well integrated withthe pro...
详细信息
ISBN:
(纸本)9781605587349
Object versioning refers to how an application can have access to previous states of its objects Implementing this mechanism is hard because it needs to be efficient in space and time, and well integrated withthe programminglanguage. this paper presents HistOOry, an object versioning system that uses an efficient data structure to store and retrieve past states. It needs only three primitives, and existing code does not need to be modified to be versioned It provides fine-grained control over what parts of objects are versioned and when It stores all states, past and present, in memory. Code can be executed in the past of the system and will see the complete system at that point in time. We have implemented our model in Smalltalk and used it for three applications that need versioning: checked postconditions, stateful execution tracing and a planar point location implementation. Benchmarks are provided to asses the practical complexity of our implementation.
Building concurrent shared-memory data structures is a notoriously difficult problem, and so the widespread move to multi-core and multi-processor hardware has led to increasing interest in language constructs that ma...
详细信息
ISBN:
(纸本)9781605583792
Building concurrent shared-memory data structures is a notoriously difficult problem, and so the widespread move to multi-core and multi-processor hardware has led to increasing interest in language constructs that may make concurrent programming easier. One technique that has been studied widely is the use of atomic blocks built over transactional memory (TM): the programmer marks a section of code as atomic, and the languageimplementation speculatively executes it using transactions. Transactions can run in parallel so long as they access different *** this talk I'll introduce some of the challenges that I've seen in building robust implementations of this idea. What are the languagedesign choices that exist? What language features can be used inside atomic blocks, and where can atomic blocks occur? Which uses of atomic blocks should be considered correct, and which uses should be considered "racy"? What are the likely impacts of different design choices on performance? What are the impacts on flexibility for the language implementer, and what are the impacts on flexibility to the programmer using these constructs?I'll argue that one way of trying to resolve these questions is to be rigorous about keeping the ideas of atomic blocks and TM separate; in practice they've often been conflated (not least in languages that I've worked on). I'll argue that, when thinking about atomic blocks, we should keep a wide range of possible implementations in mind (for example, TM, lock inference, or simply control over pre-emption). Similarly, when thinking about TM, we should recognize that it can be exposed to programmers through a wide range of abstractions and language constructs.
the complexity of the well-explored regions of the programminglanguagedesign space has increased substantially in the last twenty-five years withthe addition of a large number of object-oriented programming languag...
详细信息
We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type theory. that origina...
详细信息
ISBN:
(纸本)9781605583327
We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type theory. that original system was a proof of concept, where every program verification was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source files, showcasing the versatility of that proof assistant as a platform for research on languagedesign and verification. Both versions of the system have been evaluated with case studies in the verification of imperative data structures, such as hash tables with higher-order iterators. the verification burden in our new system is reduced by at least an order of magnitude compared to the old system, by replacing manual proof with automation. the core of the automation is a simplification procedure for implications in higher-order separation logic, with hooks that allow programmers to add domain-specific simplification rules. We argue for the effectiveness of our infrastructure by verifying a number of data structures and a packrat parser, and we compare to similar efforts within other projects. Compared to competing approaches to data structure verification, our system includes much less code that must be trusted;namely, about a hundred lines of Coq code defining a program logic. All of our theorems and decision procedures have or build machine-checkable correctness proofs from first principles, removing opportunities for tool bugs to create faulty verifications.
暂无评论