Tags: mukul-rathi/bolt
Tags
Stripped back version of Bolt This is before inheritance, method overloading + overriding, generics
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.
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.