202 research outputs found
On the Elimination of Hypotheses in Kleene Algebra with Tests
No full textThe validity problem for certain universal Horn formulas of Kleene algebra with tests (KAT) can be efficiently reduced to the equational theory. This reduction is known as elimination of hypotheses. Hypotheses are used to describe the interaction of atomic programs and tests and are an essential component of practical program verification with KAT. The ability to eliminate hypotheses of a certain form means that the Horn theory with premises of that form remains decidable in PSPACE. It was known (Cohen 1994, Kozen and Smith 1996, Kozen 1997) how to eliminate hypotheses of the form q=0. In this paper we show how to eliminate hypotheses of the form cp=c for atomic p. Hypotheses of this form are useful in eliminating redundant code and arise quite often in the verification of compiler optimizations (Kozen and Patron 2000)
On Two Letters versus Three
No full textIf A is a context-free language over a two-letter alphabet, then the set of all words obtained by sorting words in A and the set of all permutations of words in A are context-free. This is false over alphabets of three or more letters. Thus these problems illustrate a difference in behavior between twoand three-letter alphabets. The following problem appeared on a recent exam at Cornell: Let be a finite alphabet with a fixed total ordering on the letters. For a string x 2, let sort x be the string obtained by sorting the letters in increasing order. For example, if a < b < c, then sort abacbaa = aaaabbc. ForA, let sortA = fsortx j x 2 Ag. Of the following three statements, two are false and one is true. Give counterexamples for the two false ones and a proof of the true one. (i) If A is regular, then so is sort A. (ii) If A is context-free, then so is sort A. (iii) If A is context-sensitive, then so is sort A. One might also ask the same questions about perm A, the set of all permutations of words in A. Of course, it is (i) and (ii) that are false, since sort (abc) = perm (abc) \ a b c = fa n b n c n j n 0g: 1 Interestingly, (ii) is true for both sort and perm over a two-letter alphabet. This is quite surprising: whereas a two-letter alphabet is exponentially more succinct than a one-letter alphabet, one does not normally think of a break in behavior between two- and three-letter alphabets. In many applications, three letters (or for that matter any fixed finite number of letters) can be coded into two with only a linear loss of efficiency. Not so, apparently, in this case. In this short note we give an elementary proof of these facts. The proof for sort is a fairly straightforward construction relying on Parikh’s theorem and Pilling normal form, but the proof for perm is somewhat more involved, requiring a bit of linear algebra over integer lattices. Let =fa 1�::: �adg, and let: ! N d be the Parikh map (x) de
Complexity of Boolean algebras
No full textAbstractWe show that the elementary theory of Boolean algebras is ⩽log-complete for the Berman complexity class ⋃c<ω STA(∗, 2cn, n), the class of sets accepted by alternating Turing machines running in time 2cn for some constant c and making at most n alternations on inputs of length n; thus the theory is computationally equivalent to the theory of real addition with order. We extend the completeness results to various subclasses of Boolean algebras, including the finite, free, atomic, atomless, and complete Boolean algebras. Finally we show that the theory of any finite collection of finite Boolean algebras is complete for PSPACE, while the theory of any other collection is ⩽log-hard for ⋃c<ω STA(∗, 2cn, n)
Programming Safely with Weak (and Strong) Consistency
No full text364 pagesWriting programs against weak consistency is inherently difficult. This dissertation makes the job of writing safe programs against weak consistency easier, by introducing programming languages in which strong guarantees are defended from weakly-consistent influence, and in which programmers can write consistent-by-construction programs atop underlying weakly-consistent replication. The first of these languages is MixT, a new language for writing mixed-consistency transactions. These atomic transactions can operate against data at multiple consistency levels simultaneously, and are equipped with an information-flow type system which guarantees weakly-consistent observations cannot influence strongly-consistent actions. While mixed-consistency transactions can defend strong data from weak observations, they cannot ensure that fully-weak code is itself correct. To address this, we leverage monotonic data types to introduce a core language of datalog-like predicates and triggers. In this language, programmers can write monotonic functions over a set of monotonic shared objects, ultimately resulting in a boolean. These monotonic, boolean-returning functions are stable predicates: once they have become true, they remain true for all time. Actions which are predicated on these stable predicates cannot be invalidated by missed or future updates. This monotonic language sits at the core of Derecho, a new system for building strongly-consistent distributed systems via replicated state machines. Derecho's Shared State Table (SST) implements monotonic datatypes atop Remote Direct Memory Access (RDMA), resulting in a high-performance, asynchronous substrate on which to build Derecho's monotonic language. Using this SST, we have rephrased the Paxos delivery condition monotonically, granting strong consistency despite the underlying asynchronous replication. Finally Gallifrey exposes the monotonic reasoning properties of Derecho's core language directly to the user, safely integrating monotonic datatypes into a traditional Java-like programming language. Gallifrey allows any object to be asynchronously replicated via restrictions to its interface, allowing only those operations which are safe to call concurrently. Datatypes shared under these restrictions can be viewed monotonically, using a language of predicates and triggers similar to that at the core of Derecho. A novel linear region-based type system enforces that shared object restrictions are respected
Mechanisms for Provable Integrity Protection in Decentralized Systems
No full text284 pagesDecentralized systems are built from a set of coordinating independent services. Yet these services might not trust each other, making it difficult to maintain the integrity of the whole application. This dissertation explores two different approaches to achieving provable integrity guarantees in such systems. The first technique, realized in Solidus, applies cryptographic tools to provably preserve the integrity of a blockchain-based financial transaction system while hiding the sender, receiver, and value of each transaction. The second complements the cryptographic approach by showing how to achieve strong integrity guarantees for realistic systems using language-based Information Flow Control (IFC). Traditional IFC systems only provide strong integrity guarantees in the absence of endorsement---treating inputs as more trusted than their source---but endorsement is necessary in real-world systems. This work classifies two ways in which unrestricted endorsements can compromise system integrity if attackers violate implicit assumptions. In both cases, IFC ideas help define security and support language-based rules to provably eliminate all attacks in the class
Toward the Automation of Category Theory
No full textWe introduce a sequent system for basic category-theoretic reasoning
suitable for computer implementation. We illustrate its use by giving a complete formal proof that the functor categories Fun[CxD,E] and Fun[C,Fun[D,E]] are naturally isomorphic
On Distance Coloring
No full textCall a connected undirected graph (d,c)-colorable if there is a vertex coloring using at most c colors such that no two vertices of distance d or less have the same color. It is well known that (1,2)-colorability is decidable in linear time, but (1,c)-colorability for c greater than or equal to 3 is NP-complete. Sharp (2007) shows that for fixed d greater than or equal to 2, the (d,c)-colorability problem is solvable in linear time for c less than or equal to 3d/2 and NP-complete otherwise. In this note we give an alternative construction that improves the upper time bound as a function of d for the case c less than or equal to 3d/2. The construction entails a generalization of the notion of tree decomposition and bounded treewidth (Robertson and Seymour 1986) to arbitrary overlay graphs, not just trees, which may be of independent interest
Composable Compilers: Evolution toward a Practical Reality
No full textThe ability to add new features to programming languages is essential for language design experimentation and domain-specific developments, but implementing and maintaining small language extensions in traditional compilers remain a challenge. General-purpose programming languages do not have desired mechanisms to integrate small, independently developed extensions into a working programming language. At the same time, domain-specific languages that support such integration struggle to gain popularity in the programming language community. More language mechanisms and tools are needed as a middle ground so that a broader range of programmers can implement, maintain, and combine compilers for individual language features more easily.
At the heart of compiler construction, new design patterns are proposed to allow compilers to be extended in a modular way and to be merged with little effort. These design patterns, implementable in a mainstream programming language, encode dynamic relationships between node types in abstract syntax trees (ASTs) so that inheritance in object-oriented programming still works over the course of language evolution. A new AST representation lets a single AST be viewed as different programs for different languages. Compiler passes are language-neutral, making translations reusable and composable.
At the front end, engineering language syntax can be a painstaking process, especially when individual language syntaxes start to interact. Automatic parser generators, albeit a powerful tool to parse complex grammars, are unhelpful when grammars are faulty, as reports of parsing conflicts do not explain these faults. To improve debugging experience, a semi-decision procedure is added to an LALR parser generator to give compact counterexamples illustrating why the grammar in question is ambiguous. For unambiguous grammars that cause parsing conflicts, a different kind of counterexample is constructed to aid removal of conflicts.
At the back end, translation passes in compilers require extracting components of AST nodes. Pattern matching, an important feature in functional languages, is a prime candidate for this task. However, data abstraction and extensibility, two concepts central to object-oriented languages, are in conflict with pattern matching. A new language design based on modal abstraction reconciles static, modular reasoning about exhaustiveness in pattern matching with data abstraction
Sound And Practical Methods For Full-System Timing Channel Control
No full textBuilding systems with rigorous security guarantees is difficult, because most programming languages lack support for reasoning about security. This situation is amplified by emerging timing attacks, which reveal secrets from computation time. Recent work shows that timing channels can quickly leak sensitive information, such as private keys of RSA and AES. Such threats greatly harm the security of many emerging applications, such as cloud computing, mobile computing, and embedded systems. This dissertation describes novel programming languages and run-time enforcement mechanisms for full-system control of timing channels. The proposed approach has two major components: A new software-hardware security interface, and control mechanisms present at separate levels of system abstraction. These control mechanisms include: 1) A type system for an imperative language, so that well-typed programs provably leak only a bounded amount of information via timing channels, 2) SecVerilog, a hardware description language that supports mostly-static, precise reasoning about information flows in hardware designs, and 3) Predictive mitigation, a general run-time mechanism that permits tunable tradeoffs between security and performance. Evaluation on real-world security-sensitive applications suggest that the proposed approach is sound and has reasonable performance
- …
