-
PSM: Policy Synchronised Deterministic Memory
Authors:
Michael Mendler,
Marc Pouzet
Abstract:
Concurrency and determinacy do not go well with each other when resources must be shared. Haskell provides parallel programming abstractions such as IVar and LVar in the Par monad and concurrent abstractions such as MVar and TVar in the in IO and STM monads, respectively. The former are determinate but have no destructive updates and the latter have destructive updates but do not guarantee determi…
▽ More
Concurrency and determinacy do not go well with each other when resources must be shared. Haskell provides parallel programming abstractions such as IVar and LVar in the Par monad and concurrent abstractions such as MVar and TVar in the in IO and STM monads, respectively. The former are determinate but have no destructive updates and the latter have destructive updates but do not guarantee determinacy. Programming patterns that are both concurrent and determinate, such as those provided by Kahn or Berry require memory abstractions at a higher level than is currently available. In this paper we describe a new type context PSM for policy synchronised memory in Haskell. Like STM and IO, the computations in PSM can access persistent state and, as a side-effect, update the memory in imperative style. Like the Par and IO monads, PSM supports concurrent threads and shared state. However, in contrast to IO, our PSM contexts are race-free since concurrent accesses are policy coordinated which guarantees determinacy.Well-typed transactions in the PSM context can accommodate abstract data structures that are imperative, concurrently shareable and still behave deterministically, by construction.
△ Less
Submitted 18 June, 2025;
originally announced June 2025.
-
On the ABK Conjecture, alpha-well Quasi Orders and Dress-Schiffels product
Authors:
Uri Abraham,
Robert Bonnet,
Mirna Džamonja,
Maurice Pouzet
Abstract:
The following is a 2008 conjecture of Abraham, Bonnet and Kubiś: [ABK Conjecture] Every well quasi order (wqo) is a countable union of better quasi orders (bqo). We obtain a partial progress on the conjecture, by showing that the class of orders that are a countable union of better quasi orders (sigma-bqo) is closed under various operations. These include diverse products, such as the Dress-Shieff…
▽ More
The following is a 2008 conjecture of Abraham, Bonnet and Kubiś: [ABK Conjecture] Every well quasi order (wqo) is a countable union of better quasi orders (bqo). We obtain a partial progress on the conjecture, by showing that the class of orders that are a countable union of better quasi orders (sigma-bqo) is closed under various operations. These include diverse products, such as the Dress-Shieffels product. We develop various properties of the latter product. In relation with the main question, we explore the class of alpha-wqo for countable ordinals alpha and obtain several closure properties and a Hausdorff-style classification theorem. Our main contribution is the discovery of various properties of sigma-bqos and ruling out potential counterexamples to the ABK Conjecture.
△ Less
Submitted 25 January, 2025; v1 submitted 20 March, 2023;
originally announced March 2023.
-
Hereditary rigidity, separation and density In memory of Professor I.G. Rosenberg
Authors:
Lucien Haddad,
Masahiro Miyakawa,
Maurice Pouzet,
Hisayuki Tatsumi
Abstract:
We continue the investigation of systems of hereditarily rigid relations started in Couceiro, Haddad, Pouzet and Schölzel [1]. We observe that on a set $V$ with $m$ elements, there is a hereditarily rigid set $\mathcal R$ made of $n$ tournaments if and only if $m(m-1)\leq 2^n$. We ask if the same inequality holds when the tournaments are replaced by linear orders. This problem has an equivalent fo…
▽ More
We continue the investigation of systems of hereditarily rigid relations started in Couceiro, Haddad, Pouzet and Schölzel [1]. We observe that on a set $V$ with $m$ elements, there is a hereditarily rigid set $\mathcal R$ made of $n$ tournaments if and only if $m(m-1)\leq 2^n$. We ask if the same inequality holds when the tournaments are replaced by linear orders. This problem has an equivalent formulation in terms of separation of linear orders. Let $h_{\rm Lin}(m)$ be the least cardinal $n$ such that there is a family $\mathcal R$ of $n$ linear orders on an $m$-element set $V$ such that any two distinct ordered pairs of distinct elements of $V$ are separated by some member of $\mathcal R$, then $ \lceil \log_2 (m(m-1))\rceil\leq h_{\rm Lin}(m)$ with equality if $m\leq 7$. We ask whether the equality holds for every $m$. We prove that $h_{\rm Lin}(m+1)\leq h_{\rm Lin}(m)+1$. If $V$ is infinite, we show that $h_{\rm Lin}(m)= \aleph_0$ for $m\leq 2^{\aleph_0}$. More generally, we prove that the two equalities $h_{\rm Lin}(m)= log_2 (m)= d({\rm Lin}(V))$ hold, where $\log_2 (m)$ is the least cardinal $μ$ such that $m\leq 2^μ$, and $d({\rm Lin}(V))$ is the topological density of the set ${\rm Lin}(V)$ of linear orders on $V$ (viewed as a subset of the power set $\mathcal{P}(V\times V)$ equipped with the product topology). These equalities follow from the {\it Generalized Continuum Hypothesis}, but we do not know whether they hold without any set theoretical hypothesis.
△ Less
Submitted 1 April, 2021;
originally announced April 2021.
-
Reactive Probabilistic Programming
Authors:
Guillaume Baudart,
Louis Mandel,
Eric Atkinson,
Benjamin Sherman,
Marc Pouzet,
Michael Carbin
Abstract:
Synchronous modeling is at the heart of programming languages like Lustre, Esterel, or Scade used routinely for implementing safety critical control software, e.g., fly-by-wire and engine control in planes. However, to date these languages have had limited modern support for modeling uncertainty -- probabilistic aspects of software's environment or behavior -- even though modeling uncertainty is a…
▽ More
Synchronous modeling is at the heart of programming languages like Lustre, Esterel, or Scade used routinely for implementing safety critical control software, e.g., fly-by-wire and engine control in planes. However, to date these languages have had limited modern support for modeling uncertainty -- probabilistic aspects of software's environment or behavior -- even though modeling uncertainty is a primary activity when designing a control system.
In this paper we present ProbZelus the first synchronous probabilistic programming language. ProbZelus conservatively provides the facilities of a synchronous language to write control software, with probabilistic constructs to model uncertainties and perform inference-in-the-loop.
We present the design and implementation of the language. We propose a measure-theoretic semantics of probabilistic stream functions and a simple type discipline to separate deterministic and probabilistic expressions. We demonstrate a semantics-preserving compilation into a first-order functional language that lends itself to a simple presentation of inference algorithms for streaming models. We also redesign the delayed sampling inference algorithm to provide efficient streaming inference. Together with an evaluation on several reactive applications, our results demonstrate that ProbZelus enables the design of reactive probabilistic applications and efficient, bounded memory inference.
△ Less
Submitted 9 April, 2020; v1 submitted 20 August, 2019;
originally announced August 2019.
-
Injective envelopes of transition systems and Ferrers languages
Authors:
Mustapha Kabil,
Maurice Pouzet
Abstract:
We consider reflexive and involutive transition systems over an ordered alphabet $A$ equipped with an involution. We give a description of the injective envelope of any two-element set in terms of Galois lattice, from which we derive a test of its finiteness. Our description leads to the notion of Ferrers language.
We consider reflexive and involutive transition systems over an ordered alphabet $A$ equipped with an involution. We give a description of the injective envelope of any two-element set in terms of Galois lattice, from which we derive a test of its finiteness. Our description leads to the notion of Ferrers language.
△ Less
Submitted 4 July, 2019;
originally announced July 2019.
-
Sundials/ML: Connecting OCaml to the Sundials Numeric Solvers
Authors:
Timothy Bourke,
Jun Inoue,
Marc Pouzet
Abstract:
This paper describes the design and implementation of a comprehensive OCaml interface to the Sundials library of numeric solvers for ordinary differential equations, differential algebraic equations, and non-linear equations. The interface provides a convenient and memory-safe alternative to using Sundials directly from C and facilitates application development by integrating with higher-level lan…
▽ More
This paper describes the design and implementation of a comprehensive OCaml interface to the Sundials library of numeric solvers for ordinary differential equations, differential algebraic equations, and non-linear equations. The interface provides a convenient and memory-safe alternative to using Sundials directly from C and facilitates application development by integrating with higher-level language features, like garbage-collected memory management, algebraic data types, and exceptions. Our benchmark results suggest that the interface overhead is acceptable: the standard examples are rarely twice as slow in OCaml than in C, and often less than 50% slower. The challenges in interfacing with Sundials are to efficiently and safely share data structures between OCaml and C, to support multiple implementations of vector operations and linear solvers through a common interface, and to manage calls and error signalling to and from OCaml. We explain how we overcame these difficulties using a combination of standard techniques such as phantom types and polymorphic variants, and carefully crafted data representations.
△ Less
Submitted 30 December, 2018;
originally announced December 2018.
-
A Type System for the Automatic Distribution of Higher-order Synchronous Dataflow Programs
Authors:
Gwenaël Delaval,
Alain Girault,
Marc Pouzet
Abstract:
We address the design of distributed systems with synchronous dataflow programming languages. As modular design entails handling both architectural and functional modularity, our first contribution is to extend an existing synchronous dataflow programming language with primitives allowing the description of a distributed architecture and the localization of some expressions onto some processors. W…
▽ More
We address the design of distributed systems with synchronous dataflow programming languages. As modular design entails handling both architectural and functional modularity, our first contribution is to extend an existing synchronous dataflow programming language with primitives allowing the description of a distributed architecture and the localization of some expressions onto some processors. We also present a distributed semantics to formalize the distributed execution of synchronous programs. Our second contribution is to provide a type system, in order to infer the localization of non-annotated values by means of type inference and to ensure, at compilation time, the consistency of the distribution. Our third contribution is to provide a type-directed projection operation to obtain automatically,from a centralized typed program, the local program to be executed by each computing resource. The type system as well as the automatic distribution mechanism has been fully implemented in the compiler of an existing synchronous data-flow programming language.
△ Less
Submitted 12 November, 2012;
originally announced November 2012.
-
N-free extensions of posets.Note on a theorem of P.A.Grillet
Authors:
Maurice Pouzet,
Nejib Zaguia
Abstract:
Let $S\_{N}(P)$ be the poset obtained by adding a dummy vertex on each diagonal edge of the $N$'s of a finite poset $P$. We show that $S\_{N}(S\_{N}(P))$ is $N$-free. It follows that this poset is the smallest $N$-free barycentric subdivision of the diagram of $P$, poset whose existence was proved by P.A. Grillet. This is also the poset obtained by the algorithm starting with $P\_0:=P$ and consi…
▽ More
Let $S\_{N}(P)$ be the poset obtained by adding a dummy vertex on each diagonal edge of the $N$'s of a finite poset $P$. We show that $S\_{N}(S\_{N}(P))$ is $N$-free. It follows that this poset is the smallest $N$-free barycentric subdivision of the diagram of $P$, poset whose existence was proved by P.A. Grillet. This is also the poset obtained by the algorithm starting with $P\_0:=P$ and consisting at step $m$ of adding a dummy vertex on a diagonal edge of some $N$ in $P\_m$, proving that the result of this algorithm does not depend upon the particular choice of the diagonal edge choosen at each step. These results are linked to drawing of posets.
△ Less
Submitted 13 September, 2005;
originally announced September 2005.
