search

AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Apache License 2.0
104 stars 6 forks source link

Improve performance by reimplementation #1000

Open treiher opened 2 years ago

treiher commented 2 years ago

Context and Problem Statement

The use of Python makes RecordFlux much slower than it could be. In particular, the model verification and the code generation could be significantly improved by using a more performant programming language. A partial reimplementation of some of the most affected parts could be a good first step. We have already had good experience by switching from Python to Ada for the specification parsing (using langkit).

Considered Options

O1 Ada

+ Fast − Few reusable libraries

O2 Rust

+ Fast + Several reusable libraries (e.g., for representing graph structure in messages)

Decision Outcome

TBD

kanigsson commented 2 years ago

Some other points and a new option:

O1 Ada

+ Used extensively at AdaCore - Not particularly suited for AST representation

O2 Rust

- Used very little at AdaCore currently (?) - Not particularly suited for AST representation(?)

O3 OCaml

+ Used to some extent at AdaCore + Particularly well-suited for AST manipulations + Langkit API exists (to be double-checked) + Strong typing - Probably slower than Ada/Rust, but much faster than Python