May 22 2018 cs.PL
One Monad to Prove Them All is a modern fairy tale about curiosity and perseverance, two important properties of a successful PhD student. We follow the PhD student Mona on her adventurous journey of proving properties about Haskell programs in the proof assistant Coq. In quest for a solution Mona goes on an educating journey through the land of functional programming. We follow her on her journey when she learns about concepts like free monads and containers as well as basics and restrictions of proof assistants like Coq. These concepts are well-known individually, but their interplay gives rise to a solution for Mona's problem that has not been presented before. More precisely, Mona's final solution does not only work for a specific monad instance but even allows her to prove monad-generic properties. That is, instead of proving properties over and over again for specific monad instances she is able to prove properties that hold for all monads. In the end of her journey Mona comes to the land of functional logic and the land of probabilistic programming. She learns that, because her proofs are monad-generic, they even hold in languages with other effects like non-determinism or probabilism. If you are a citizen of the land of functional programming or are at least familiar with its customs, had a journey that involved reasoning about functional programs of your own, or are just a curious soul looking for the next story about monads and proofs, then this tale is for you.
Weak memory models are a consequence of the desire on part of architects to preserve all the uniprocessor optimizations while building a shared memory multiprocessor. The efforts to formalize weak memory models of ARM and POWER over the last decades are mostly empirical -- they try to capture empirically observed behaviors -- and end up providing no insight into the inherent nature of weak memory models. This paper takes a constructive approach to find a common base for weak memory models: we explore what a weak memory would look like if we constructed it with the explicit goal of preserving all the uniprocessor optimizations. We will disallow some optimizations which break a programmer's intuition in highly unexpected ways. The constructed model, which we call General Atomic Memory Model (GAM), allows all four load/store reorderings. We give the construction procedure of GAM, and provide insights which are used to define its operational and axiomatic semantics. Though no attempt is made to match GAM to any existing weak memory model, we show by simulation that GAM has comparable performance with other models. No deep knowledge of memory models is needed to read this paper.
May 22 2018 cs.PL
That the Haskell Compiler GHC is capable of proving non-trivial equalities between Haskell code, by virtue of its aggressive optimizer, in particular the term rewriting engine in the simplifier. We demonstrate this with a surprising little code in a GHC plugin, explains the knobs we had to turn, discuss the limits of the approach and related applications of the same idea, namely testing that promises from Haskell libraries with domain-specific optimizations hold.
May 22 2018 cs.PL
QR decomposition is used prevalently in wireless communication. In this paper, we express the Givens-rotation-based QR decomposition algorithm on a spatial architecture using T2S (Temporal To Spatial), a high-productivity spatial programming methodology for expressing high-performance spatial designs. There are interesting challenges: the loop iteration space is not rectangular, and it is not obvious how the imperative algorithm can be expressed in a functional notation, the starting point of T2S. Using QR decomposition as an example, this paper elucidates some general principle, and de-mystifies high-performance spatial programming. The paper also serves as a tutorial of spatial programming for programmers who are not mathematicians, not expert programmers, and not experts on spatial architectures, but still hope to intuitively identify a high-performance design and map to spatial architectures efficiently.