Morrisett, Greg Gregory

Person:
Morrisett, Greg Gregory

Last Name

Morrisett

First Name

Greg Gregory

Name

Morrisett, Greg Gregory

Full item page

Search Results

Now showing 1 - 10 of 30

Dependent type theory of stateful higher-order functions
(2005) Nanevski, Aleksandar; Morrisett, Greg Gregory
In this paper we investigate a logic for reasoning about programs with higher-order functions and effectful features like non-termination and state with aliasing. We propose a dependent type theory HTT (short for Hoare Type Theory), where types serve as program specifications. In case of effectful programs, the type of Hoare triples {P}x:A{Q} specifies the precondition P, the type of the return result A, and the postcondition Q. By Curry-Howard isomorphism, a dependent type theory may be viewed as a functional programming language. From this perspective, the type of Hoare triples is a monad, and HTT is a monadic language, whose pure fragment consists of higher-order functions, while the effectful fragment is a full Turing-complete imperative language with conditionals, loops, recursion and commands for stateful operations like allocation, lookup and mutation of location content.
Evaluating Value-Graph Translation Validation for LLVM
(2011) Tristan, Jean-Baptiste F.; Govereau, Paul; Morrisett, Greg Gregory
Translation validators are static analyzers that attempt to verify that program transformations preserve semantics. Normalizing trans- lation validators do so by trying to match the value-graphs of an original function and its transformed counterpart. In this paper, we present the design of such a validator for LLVM’s intra-procedural optimizations, a design that does not require any instrumentation of the optimizer, nor any rewriting of the source code to compile, and needs to run only once to validate a pipeline of optimizations. We present the results of our preliminary experiments on a set of bench- marks that include GCC, a perl interpreter, SQLite3, and other C programs.
Type-theoretic Semantics for Transactional Concurrency
(2007) Nanevski, Aleksandar; Govereau, Paul; Morrisett, Greg Gregory
We propose a dependent type theory that combines programming, specifications and reasoning about higher-order concurrent programs with shared higher-order transactional memory. We build on our previous work on Hoare Type Theory (HTT), which is extended here with types that correspond to Hoare-style specifications for transactions. The new types have the form CMD {I}{P} x:A{Q}, and classify concurrent programs that may execute in a shared state with invariant I, and local state precondition P. Upon termination, such programs return a result of type A, and local state changed according to the postcondition Q. Throughout the execution, shared state always satisfies the invariant I, except at specific critical sections which are executed atomically; that is, sequentially, without interference from other processes. Atomic sections may violate the invariant, but must restore it upon exit. We follow the idea of Separation Logic, and adopt “small footprint” specifications, whereby each process is associated with a precondition that tightly describes its state requirement. HTT is a program logic and a dependently typed programming language at the same time. To consider it as a logic, we prove that it is sound and compositional. To consider it as a programming language, we define its operational semantics, and show adequacy with respect to the specifications.
Abstract Predicates and Mutable ADTs in Hoare Type Theory
(2006) Nanevski, Aleksandar; Ahmed, Amal; Morrisett, Greg Gregory; Birkedal, Lars
Hoare Type Theory (HTT) combines a dependently typed, higher-order language with monadically-encapsulated, stateful computations. The type system incorporates pre- and post-conditions, in a fashion similar to Hoare and Separation Logic, so that programmers can modularly specify the requirements and effects of computations within types. This paper extends HTT with quantification over abstract predicates (i.e., higher-order logic), thus embedding into HTT the Extended Calculus of Constructions. When combined with the Hoare-like specifications, abstract predicates provide a powerful way to define and encapsulate the invariants of private state; that is, state which may be shared by several functions, but is not accessible to their clients. We demonstrate this power by sketching a number of abstract data types and functions that demand ownership of mutable memory, including an idealized custom memory manager.
Polymorphism and Separation in Hoare Type Theory
(2006) Nanevski, Aleksandar; Morrisett, Greg Gregory; Birkedal, Lars
In previous work we have proposed a Dependent Hoare Type Theory (HTT) as a framework for development and reasoning about higher-order functional programs with effects of state, aliasing and nontermination. The main feature of HTT is the type of Hoare triples {P}x:A{Q} specifying computations with precondition P and postcondition Q, that return a result of type A. Here we extend HTT with predicative type polymorphism. Type quantification is possible in both types and assertions, and we can also quantify over Hoare triples. We show that as a consequence it becomes possible to reason about disjointness of heaps in the assertion logic of HTT. We use this expressiveness to interpret the Hoare triples in the “small footprint” manner advocated by Separation Logic, whereby a precondition tightly describes the heap fragment required by the computation. We support stateful commands of allocation, lookup, strong update, deallocation, and pointer arithmetic.
A Step-Indexed Model of Substructural State
(2005) Ahmed, Amal; Fluet, Matthew; Morrisett, Greg Gregory
The concept of a “unique” object arises in many emerging programming languages such as Clean, CQual, Cyclone, TAL, and Vault. In each of these systems, unique objects make it possible to perform operations that would otherwise be prohibited (e.g., deallocating an object) or to ensure that some obligation will be met (e.g., an opened file will be closed). However, different languages provide different interpretations of “uniqueness” and have different rules regarding how unique objects interact with the rest of the language. Our goal is to establish a common model that supports each of these languages, by allowing us to encode and study the interactions of the different forms of uniqueness. The model we provide is based on a substructural variant of the polymorphic λ-calculus, augmented with four kinds of mutable references: unrestricted, relevant, affine, and linear. The language has a natural operational semantics that supports deallocation of references, strong (type-varying) updates, and storage of unique objects in shared references. We establish the strong soundness of the type system by constructing a novel, semantic interpretation of the types. This technical report is really two documents in one: The first part is a paper appearing in the Tenth ACM SIGPLAN International Conference on Functional Programming (ICFP’05). The second part is a formal development of the language, step-indexed model, and soundness proof referenced in the first part. If you have already read a version of “A Step-Indexed Model of Substructural State”, then you should proceed directly to the appendices.
Preliminary Design of the SAFE Platform
(Association for Computing Machinery, 2011) Morrisett, Greg Gregory; DeHon, André; Karel, Ben; Malecha, Gregory Michael; Montagu, Benoît; Morisset, Robin; Pierce, Benjamin C.; Pollack, Randy; Ray, Sumit; Shivers, Olin; Smith, Jonathan M.; Sullivan, Gregory; Knight, Thomas F., Jr.
SAFE is a clean-slate design for a secure host architecture. It integrates advances in programming languages, operating systems, and hardware and incorporates formal methods at every step. Though the project is still at an early stage, we have assembled a set of basic architectural choices that we believe will yield a high-assurance system. We sketch the current state of the design and discuss several of these choices.
Mechanized Verification with Sharing
(Springer Verlag, 2010) Malecha, Gregory Michael; Morrisett, Greg Gregory
We consider software verification of imperative programs by theorem proving in higher-order separation logic. Separation logic is quite effective for reasoning about tree-like data structures, but less so for data structures with more complex sharing patterns. This problem is compounded by some higher-order patterns, such as stateful iterators and visitors, where multiple clients need to share references into a data structure. We show how both styles of sharing can be achieved without sacrificing abstraction using mechanized reasoning about fractional permissions in Hoare Type Theory.
Combining Control-Flow Integrity and Static Analysis for Efﬁcient and Validated Data Sandboxing
(Association for Computing Machinery, 2011) Zeng, Bin; Tan, Gang; Morrisett, Greg Gregory
In many software attacks, inducing an illegal control-flow transfer in the target system is one common step. Control-Flow Integrity (CFI) protects a software system by enforcing a pre-determined control-flow graph. In addition to providing strong security, CFI enables static analysis on low-level code. This paper evaluates whether CFI-enabled static analysis can help build efficient and validated data sandboxing. Previous systems generally sandbox memory writes for integrity, but avoid protecting confidentiality due to the high overhead of sandboxing memory reads. To reduce overhead, we have implemented a series of optimizations that remove sandboxing instructions if they are proven unnecessary by static analysis. On top of CFI, our system adds only 2.7% runtime overhead on SPECint2000 for sandboxing memory writes and adds modest 19% for sandboxing both reads and writes. We have also built a principled data-sandboxing verifier based on range analysis. The verifier checks the safety of the results of the optimizer, which removes the need to trust the rewriter and optimizer. Our results show that the combination of CFI and static analysis has the potential of bringing down the cost of general inlined reference monitors, while maintaining strong security.
Nikola: Embedding Compiled GPU Functions in Haskell
(Association for Computing Machinery, 2010) Mainland, Geoffrey; Morrisett, Greg Gregory
We describe Nikola, a first-order language of array computations embedded in Haskell that compiles to GPUs via CUDA using a new set of type-directed techniques to support re-usable computations. Nikola automatically handles a range of low-level details for Haskell programmers, such as marshaling data to/from the GPU, size inference for buffers, memory management, and automatic loop parallelization. Additionally, Nikola supports both compile-time and run-time code generation, making it possible for programmers to choose when and where to specialize embedded programs.