Spelling suggestions: "subject:"anormal methods for software"" "subject:"1normal methods for software""
1 |
Composable, Sound Transformations for Nested Recursion and LoopsKirshanthan Sundararajah (16647885) 26 July 2023 (has links)
<p> </p>
<p>Programs that use loops to operate over arrays and matrices are generally known as <em>regular programs</em>. These programs appear in critical applications such as image processing, differential equation solvers, and machine learning. Over the past few decades, extensive research has been done on composing, verifying, and applying scheduling transformations like loop interchange and loop tiling for regular programs. As a result, we have general frameworks such as the polyhedral model to handle transformations for loop-based programs. Similarly, programs that use recursion and loops to manipulate pointer-based data structures are known as <em>irregular programs</em>. Irregular programs also appear in essential applications such as scientific simulations, data mining, and graphics rendering. However, there is no analogous framework for recursive programs. In the last decade, although many scheduling transformations have been developed for irregular programs, they are ad-hoc in various aspects, such as being developed for a specific application and lacking portability. This dissertation examines principled ways to handle scheduling transformations for recursive programs through a unified framework resulting in performance enhancement. </p>
<p>Finding principled approaches to optimize irregular programs at compile-time is a long-standing problem. We specifically focus on scheduling transformations that reorder a program’s operations to improve performance by enhancing locality and exploiting parallelism. In the first part of this dissertation, we present PolyRec, a unified general framework that can compose and apply scheduling transformations to nested recursive programs and reason about the correctness of composed transformations. PolyRec is a first-of-its-kind unified general transformation framework for irregular programs consisting of nested recursion and loops. It is built on solid theoretical foundations from the world of automata and transducers and provides a fundamentally novel way to think about recursive programs and scheduling transformations for them. The core idea is designing mechanisms to strike a balance between the expressivity in representing the set of dynamic instances of computations, transformations, and dependences and the decidability of checking the correctness of composed transformations. We use <em>multi-tape </em>automata and transducers to represent the set of dynamic instances of computations and transformations, respectively. These machines are similar yet more expressive than their classical single-tape counterparts. While in general decidable properties of classical machines are undecidable for multi-tape machines, we have proven that those properties are decidable for the class of machines we consider, and we present algorithms to verify these properties. Therefore these machines provide the building blocks to compose and verify scheduling transformations for nested recursion and loops. The crux of the PolyRec framework is its regular string-based representation of dynamic instances that allows to lexicographically order instances identically to their execution order. All the transformations considered in PolyRec require different ordering of these strings representable only with <em>additive </em>changes to the strings. </p>
<p>Loop transformations such as <em>skewing </em>require performing arithmetic on the representation of dynamic instances. In the second part of this dissertation, we explore this space of transformations by introducing skewing to nested recursion. Skewing plays an essential role in producing easily parallelizable loop nests from seemingly difficult ones due to dependences carried across loops. The inclusion of skewing for nested recursion to PolyRec requires significant extensions to representing dynamic instances and transformations that facilitate <em>performing arithmetic using strings</em>. First, we prove that the machines that represent the transformations are still composable. Then we prove that the representation of dependences and the algorithm that checks the correctness of composed transformations hold with minimal changes. Our new extended framework is known as UniRec, since it resembles the unimodular transformations for perfectly nested loop nests, which consider any combination of the primary transformations interchange, reversal, and skewing. UniRec opens possibilities of producing newly composed transformations for nested recursion and loops and verifying their correctness. We claim that UniRec completely subsumes the unimodular framework for loop transformations since nested recursion is more general than loop nests. </p>
|
2 |
A TRANSLATION OF OCAML GADTS INTO COQPedro da Costa Abreu Junior (18422613) 23 April 2024 (has links)
<p dir="ltr">Proof assistants based on dependent types are powerful tools for building certified software. In order to verify programs written in a different language, however, a representation of those programs in the proof assistant is required. When that language is sufficiently similar to that of the proof assistant, one solution is to use a <i>shallow embedding</i> to directly encode source programs as programs in the proof assistant. One challenge with this approach is ensuring that any semantic gaps between the two languages are accounted for. In this thesis, we present <i>GSet</i>, a mixed embedding that bridges the gap between OCaml GADTs and inductive datatypes in Coq. This embedding retains the rich typing information of GADTs while also allowing pattern matching with impossible branches to be translated without additional axioms. We formalize this with GADTml, a minimal calculus that captures GADTs in OCaml, and gCIC, an impredicative variant of the Calculus of Inductive Constructions. Furthermore, we present the translation algorithm between GADTml and gCIC, together with a proof of the soundness of this translation. We have integrated this technique into coq-of-ocaml, a tool for automatically translating OCaml programs into Coq. Finally, we demonstrate the feasibility of our approach by using our enhanced version of coq-of-ocaml, to translate a portion of the Tezos code base into Coq.</p>
|
3 |
Automating Formal Verification of Distributed Systems via Property-Driven ReductionsChristopher Wagner (20817524) 05 March 2025 (has links)
<p dir="ltr">Distributed protocols, with their immense state spaces and complex behaviors, have long been popular targets for formal verification. Cutoff reductions offer an enticing path for verifying parameterized distributed systems, composed of arbitrarily many processes. While parameterized verification (i.e., algorithmically checking correctness of a system with an arbitrary number of processes) is generally undecidable, these reductions allow one to verify certain classes of parameterized systems by reducing verification of an infinite family of systems to that of a single finite instance. The finiteness of the resulting target system enables fully-automated verification of the entire unbounded system family. In this work, we aim to establish pathways for automated verification via cutoff reductions which emphasize a modular approach to establishing correctness.</p><p dir="ltr">First, we consider distributed, agreement-based (DAB) systems. That is, systems which are built on top of agreement protocols, such as agreement and consensus. While much attention has been paid to the correctness of the protocols themselves, relatively little consideration as been given to systems which utilize these protocols to achieve some higher-level functionality. To this end, we present the GSP model, a system model based on two types of globally-synchronous transitions: k-sender and k-maximal, the latter of which was introduced by this author. This model enables us to formalize systems built on distributed consensus and leader election, and define conditions under which such systems may be verified automatically, despite the involvement of an arbitrary number of participant processes (a problem which is generally undecidable). Further, we identify conditions under which these systems can be verified efficiently and provide proofs of their correctness developed in part by this author. We then present QuickSilver, a user-friendly framework for designing and verifying parameterized DAB systems and, on this author’s suggestion, lift the GSP decidability results to QuickSilver using this author’s notion of when the behavior of all processes in the system can be separated into sections of their control flow, called “phase analysis”.</p><p dir="ltr">Next, we address verification of systems beyond agreement-based protocols. We find that, among parameterized systems, a class of systems we refer to as star-networked systems has received limited attention as the subject of cutoff reductions. These systems combine heterogeneous client and server process definitions with both pairwise and broadcast communication, so they often fall outside the requirements of existing cutoff computations. We address these challenges in a novel cutoff reduction based on careful analysis of the interactions between a central process and an arbitrary number of peripheral client processes as they progress toward an error state. The key to our approach rests on identifying systems in which the central process coordinates primarily with a finite number of core client processes, and outside of such core clients, the system’s progress can be enabled by a finite number of auxiliary clients.</p><p dir="ltr">Finally, we examine systems that are doubly-unbounded, in particular, parameterized DAB systems that additionally have unbounded data domains. We present a novel reduction which leverages value symmetry and a new notion of data saturation to reduce verification of doubly-unbounded DAB systems to model checking of small, finite-state systems. We also demonstrate that this domain reduction can be applied beyond DAB systems, including to star-networked systems.</p><p dir="ltr">We implement our reductions in several frameworks to enable efficient verification of sophisticated DAB and star-networked system models, including the arbitration mechanism for a consortium blockchain, a simple key-value store, and a lock server. We show that, by reducing the complexity of verification problems, cutoff reductions open up avenues for the application of a variety of verification techniques, including further reduction.</p>
|
Page generated in 0.0964 seconds