AdaCore: Helping Developers Build Software that Matters
Everything we do at AdaCore is centered around helping developers build safe, secure and reliable software.
For over 25 years, we've worked with global leaders across the military and civil avionics, defense systems, air traffic management/control, space, railway, and financial services industries, building tools and providing services that ease the complex and difficult process of developing high-integrity software. As the need for truly secure and reliable applications expands into industries such as automotive, medical, energy, and IOT, we’re advancing our time-tested technologies to bring expertise and services to help a whole new generation of developers. Through our subscription-based business model and dedicated services arm, we have worked with hundreds of customers over the year on thousands of projects.
Our 120 experts worldwide in the US (New York, Lexington), France (Paris, Toulouse, Grenoble and Vannes), the UK, and Estonia, all play a role in developing state-of-the-art technologies to meet the challenges of building the highest grade of software.
Joining AdaCore is about joining a culture of innovation, openness, collaboration and dependability, which defines how we work together, with our customers and partners.
LKQL is a domain specific scripting language. Its main purpose is to be used to express code checkers on the languages that LKQL handles (mainly Ada, C, Python, etc).
Here is an example of a very simple LKQL check, that will check that Ada code contains goto statements:
fun goto_statements(node) = node is GotoStmt
LKQL is used to express all the checks of the new version of GNATCheck (see https://www.adacore.com/gnatpro/toolsuite/gnatcheck). While it provides unprecedented flexibility and expressivity to express new checks/customize existing checks, it's slower than we would like, which is why we would like to develop a JIT compiler for it.
Here is LKQL's reference manual.
LKQL currently has a relatively simple recursive descent interpreter, which directly explores the syntax tree produced by LKQL's parser, and interprets programs.
The goal of the internship is to develop a compiler for LKQL. The base goal is to develop a naive, fast compiler which perform no optimizations, but additional goals might be to generate more efficient code by applying a number of possible techniques:
LKQL is a dynamically typed scripting language, so every value in the naive compiler will have to be boxed, but we can envision a better compilation scheme:
LKQL uses its dynamism pretty little, and the amount of existing LKQL code is still pretty small, so we can envision adding some amount of typing to the code, in order to be able to optimize compilation further.
We can have a more traditional approach using inline caches/runtime type introspection in the interpreter in order to infer types and produce optimized code in the compiler.
The backend target is open, and might have effects on performance, both of the compiler and of the generated code. Possible options are:
Generating Ada/C code and compiling it with gcc on the fly, and then dynamically loading generated symbols. Given the amount of LKQL code, while this approach might seem inefficient, it might be totally sufficient for our needs.
Using LLVM/gcc's libjit. This might incur more work but allow us to have a more efficient compilation pipeline.
Using a JIT generation framework, such as RPython or Graal/Truffle. While those are very attractive on paper, because they will allow for a smaller effort the generation of a JIT that will probably be much faster than what we could have gotten by hand, they have other problems, most notably the fact that a lot of what exists for LKQL will have to be redeveloped/bound to be accessible from those frameworks.
The job of the intern will be to assess what the best approach is, with help, and start prototyping one or several approaches, hopefully getting conclusive enough results that we can compare the JIT's result against the baseline (the existing interpreter).
Skills required or Nice to have:
Experience with one high-level programming language (ideally Ada or Python)
Ease with UNIX command-line shell and git
Experience (academic or professional) in compilers/language front ends, or at the very least a strong interest for the topic.
Timeframe and location:
Flexible timeframe, ideally with a duration of 6 months