Skip to content

Tags: mukul-rathi/bolt

Tags

0.7.1

Toggle 0.7.1's commit message
Bolt compiler tutorials

The state of the repo after tidying up during the Bolt compiler
tutorials

simple-compiler-tutorial

Toggle simple-compiler-tutorial's commit message
Stripped back version of Bolt

This is before inheritance, method overloading + overriding, generics

0.7

Toggle 0.7's commit message
Dissertation submission

0.6

Toggle 0.6's commit message
Implement Data Race type-checker

Bolt now has a fully-functioning data-race type-checker!

Also various small tweaks to the language syntax.

0.5.1

Toggle 0.5.1's commit message
Fix LLVM Backend Bugs

Add malloc() for heap storage
Fix pthread_join() invocation bug

0.5

Toggle 0.5's commit message
Implement LLVM Compiler Backend

0.4

Toggle 0.4's commit message
Compile frontend to serialisable IR

This update  takes the typed AST and desugars it, then simplifies the IR to be serialised into Protobuf format.

0.3

Toggle 0.3's commit message
Update Pauli to use regions

The data-race type-checker now diverges from Kappa.
The language Bolt has dropped traits in favour of (in future!) class-based inheritance.

Capabilities are associated with regions, and methods are tagged with their region effects.

Unlike Kappa, composition of regions is inferred (no explicit conjunction/disjunction specified by
programmer).

Method / Function parameters can optionally be tagged with the regions they are accessing, for
fine-grained concurrency - two functions could be accessing disjoint parts of the object, and
thus their type signature would indicate it is fine to execute them concurrently.

0.2

Toggle 0.2's commit message
Make Bolt much more expressive and object-oriented

Add boolean types
Replace lambda functions with top-level function declarations
Add binary operators
Add methods to classes
Add control flow - for/while loops and if-else statements

0.1

Toggle 0.1's commit message
Core project implementation complete

A summary of Bolt:

Capabilities: linear, thread, read

Traits have a capability associated with them, and consist of a list of required fields.

Classes implement a single trait and associated capability and consist of a list of directly-accessible fields.

Bolt's expression syntax was inspired by Slang in 1B Compilers Construction, supporting first-order functions and structured fork-join concurrency through finish-async construct.

Bolt's type-checker performs full type inference.

The data-race type-checker enforces each of the capabilities, as well as enforcing that a given alias to a mutable object can only be accessed in a single thread.

The interpreter translates the typed AST to bytecode executed on a stack machine, with a thread pool where each thread has a local stack and there is a global heap, and the threads are scheduled manually. The interpreter runs in OCaml.

The expect tests consist of Bolt programs and their outputs for each of the stages: parsing, type-checking, data-race type-checking and for the execution trace of the interpreter. A subset of these contain data-races and are flagged as such by the data-race type-checker.