The PARKAS group runs and contributes to several software projects.
Find us on GitHub.
Synchronous programming with ODEs.
Zélus is an experimental language for simulating hybrid systems. It is a first-order synchronous language without clocks that has been augmented with first-order Ordinary Differential Equations (ODEs) that can be reset. Hybrid programs are compiled into the discrete subset and executed by an external numerical solver; currently the Sundials CVODE solver via an OCaml Interface.
Hunting concurrency compiler bugs.
Compilers sometimes generate correct sequential code but break the concurrency memory model of the programming language: these subtle compiler bugs are observable only when the miscompiled functions interact with concurrent contexts, making them particularly hard to detect. The cmmtest tool performs differential testing to hunt concurrency compiler bugs in C and C++ compilers against the C11/C++11 memory model. The tool has identified several mistaken write introductions and other unexpected behaviours in the latest release of the gcc compiler.
Contributions to the GNU Compiler Collection.
Licence: GPLv3+ and LGPLv3+
The GNU Compiler Collection includes front ends for C, C++, Objective-C, Fortran, Java, Ada, and Go, as well as libraries for these languages (libstdc++, libgcj,...). GCC was originally written as the compiler for the GNU operating system. The GNU system was developed to be 100% free software, free in the sense that it respects the user's freedom.
PARKAS contributes to the polyhedral compilation framework, Graphite. The team also distributes OpenStream, an experimental stream-programming extension of OpenMP, borrowing key design elements from synchronous and data-flow languages. Members of the team contributed to the design and implementation of the induction variable analysis framework of GCC.
Lustre with discrete controller synthesis and arrays.
Heptagon is a synchronous dataflow language whose syntax and semantics is inspired from Lustre, with a syntax allowing the expression of control structures (e.g., switch or mode automata).
Heptagon is also a research compiler, whose aim is to facilitate experimentation. The current version of the compiler includes the following features:
Inclusion of discrete controller synthesis within the compilation: the language is equipped with a behavioral contract mechanisms, where assumptions can be described, as well as an "enforce" property part. The semantics of this latter is that the property should be enforced by controlling the behaviour of the node equipped with the contract. This property will be enforced by an automatically built controller, which will act on free controllable variables given by the programmer. This extension has been named BZR in previous works.
Expression and compilation of array values with modular memory optimization. The language allows the expression and operations on arrays (access, modification, iterators). With the use of location annotations, the programmer can avoid unnecessary array copies.
Heptagon is developed in the Parkas (ENS) and Pop-Art (LIG/INRIA) research teams.
Integer Set Library.
Licence: MIT
isl is a library for manipulating sets and relations of integer points bounded by linear constraints. Supported operations on sets include intersection, union, set difference, emptiness check, convex hull, (integer) affine hull, integer projection, and computing the lexicographic minimum using parametric integer programming. It also includes an ILP solver based on generalized basis reduction and transitive closure computation heuristics. It comes with a state-of-the-art code generator and supports a hybrid syntax-tree/polyhedral representation of programs.
A high-level programming language for digital circuits.
Jazz is a high-level programming language for expressing, in a concise and accurate way, large digital synchronous circuits. From a language-designer perspective, Jazz is a declarative, single-assignment, higher-order, lazy, functional, and object-oriented language with parameterized types and multi-methods.
Jazz is strongly-typed (with a type-system derived from ML-sub) and supports both the explicit and implicit declaration of variables and methods thanks to a powerful constraint-based type-inference algorithm. The syntax of Jazz and its object model are Java-like and should look familiar to any Java programmer.
Contributions to the LLVM Compiler Infrastructure.
Licence: University of Illinois/NCSA Open Source License
LLVM is a collection of modular and reusable compiler and toolchain technologies. Its core libraries provide a modern source- and target-independent optimizer, along with code generation support for many CPUs. These libraries are built around a well specified code representation known as LLVM IR.
PARKAS contributes to the polyhedral compilation framework, Polly, and hosts the Polly Labs research and technology transfer in LLVM-based polyhedral compilation.
Higher-order synchronous dataflow programming.
Lucid Synchrone is an experimental language for the implementation of reactive systems. It is based on the synchronous model of time as provided by Lustre combined with some features from ML languages. The main characteristics of the language are the following:
An n-synchronous extension of Lustre.
Lucy-n is a language to program in the n-synchronous model. The language is similar to Lustre with a buffer construct. The Lucy-n compiler ensures that programs can be executed in bounded memory and automatically computes buffer sizes. Hence this language allows to program Kahn networks with bounded FIFOs.
A tool for the working semanticist.
Ott is a tool for writing definitions of programming languages and calculi. It takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It generates LaTeX to build a typeset version of the definition, and Coq, HOL, and Isabelle versions of the definition.
Polyhedral Parallel Code Generator
Licence: MIT
PPCG is our source-to-source research tool for automatic parallelization in the polyhedral model. It serves as a test bed for many compilation algorithms and heuristics published by our group, and is currently the best automatic parallelizer for CUDA and OpenCL on the Polybench suite and a variety of benchmarks.
PPCG compiles a subset of C99 with parallelization- and acceleration-friendly extensions called PENCIL. An overview paper was published at the PACT 2015 conference.
pencilcc is a more complete and integrated framework built on top of PPCG, with additional support for PENCIL, accelerated runtime interfaces to OpenCL devices, and multiple additional quirks. A tutorial recapitulates the design of PENCIL and the practical usage of pencilcc.
A programming language for interactive systems.
Compiler licence: Q Public Licence 1.0
Library licence: GNU Library General Public Licence 2.0
ReactiveML is a programming language dedicated to the implementation of interactive systems as found in graphical user interfaces, video games or simulation problems. ReactiveML is based on the synchronous reactive model of Boussinot embedded in an ML language (here Objective Caml). The synchronous reactive model provides synchronous parallel composition and dynamic features like the dynamic creation of processes. In ReactiveML, the reactive model is integrated at the language level (not as a library) which leads to safer and more natural programming.
OCaml interface to the Sundials numeric solvers.
[Sundials/ML] 1 is a comprehensive OCaml interface to the [Sundials] 2 suite of numerical solvers (CVODE, CVODES, IDA, IDAS, KINSOL, ARKODE). Its structure mostly follows that of the Sundials library, both for ease of reading the existing documentation and for adapting existing source code, but several changes have been made for programming convenience and to increase safety, namely:
OCaml versions of the standard examples usually have an overhead of about 50% compared to the original C versions, and almost never more than 100%.
A Lustre compiler in Coq
Vélus is a compiler for a subset of Lustre and Scade that is specified in Coq (with some OCaml. It integrates the CompCert C compiler to define the semantics of machine operations (integer addition, floating-point multiplication, etcetera) and to generate assembly code for different architectures. The research challenges are
This project is a collaboration with Lélio Brun, Pierre-Évariste Dagand, Paul Jeanmaire, Xavier Leroy, Marc Pouzet, and Lionel Rieg.
LaTeX package for compiling verbatim text.
User manuals and papers about programming languages usually contain many code samples, often with accompanying compiler messages giving the types of declarations or error messages explaining why certain declarations are invalid.
The checklistings package augments the fancyvrb and listings packages for including source code in LaTeX documents with a way to pass the source code through a compiler and also include the resulting messages in the document.
The motivation is to check the code samples in a document for syntax and
typing errors and to facilitate the inclusion of inferred types and compiler
warnings or errors in a text. This package is intentionally very lightweight
and unlike packages like python it is not
intended for interacting with an interpretor or including the execution
traces of code. While checklistings does not focus on a specific
programming language, it is designed to work well with ML-like languages.
The source code is available on GitHub.