Student projects

..


A Reactive Scratch compiler

MPhil/Part III (or motivated Part II) project

Context

Reactive Scratch is a programming language and IDE aimed at teaching programming to children. Reactive Scratch aims to improve Scratch, currently the most widely used platform to teach programming to schoolchildren.

Scratch is based on a very simple imperative language with structured control flow, in the style of IMP. Such a programming language is woefully inadequate for reactive programming, that is, programming where the main action of the program is to react to outside events that it does not control - which is typical of what children want to write: small video games or interactive animations. Reactive Scratch is instead based on Esterel, a reactive programming language based around the primitives of concurrency, signals, and preemption, and which was designed for reactive programming.

Currently, Reactive Scratch exists as a prototype: (1) The IDE is a fork of the Scratch IDE. The language runtime is a naive Esterel interpreter written in BuckleScript (a variant of OCaml), following the constructive operational semantics of Potop-Butucaru et al. This works fine to demonstrate the concept to other computer scientists, but is far too slow to be usable by schoolchildren. (2) Reactive Scratch does not have feature parity with Scratch: it is missing primitives to control dynamic creation and interaction of threads.

There are well-known methods to compile Esterel efficiently to circuits for embedded systems. However, (1) efficient compilation to hardware is based on concurrently executing all the parts of the program, which is expensive and undesirable for execution in a web browser, and (2) Reactive Scratch needs to extend Esterel with primitives that violate the usual assumptions about Esterel compilation.

Project

The project would involve (1) designing and writing a compiler from Reactive Scratch to circuits, and a circuit interpreter, and (2) designing and implementing primitives to make Reactive Scratch have feature parity with Scratch. The constraints of the latter are likely to strongly influence the successful design of the former. (3) Testing on actual human beings (ideally, schoolchildren, but that might be too much of an effort to organise) whether they find Reactive Scratch helpful, using qualitative methods like semi-structured interviews.

The research outcomes would be (1) the development of a new compilation method from Esterel to be executed in a web browser, and (2) of a new compilation method to support the new primitives of Reactive Scratch, and (3) if time allows, a qualitative assessment of whether people find reactive programming easier in a reactive programming language.

Requirements

The student should have a good grasp of the following topics:

Project supervisors

Jean Pichon-Pharabod and Neel Krishnaswami

(email jp622 to talk to if interested)

References

Extending a WebAssembly formalisation

MPhil/Part III and Part II projects

Context

"WebAssembly (abbreviated Wasm) is a binary instruction format for a stack-based virtual machine. Wasm is designed as a portable compilation target for programming languages, enabling deployment on the web for client and server applications."

WebAssembly is small enough to be within reach of formalisation and manipulation in proof assistants. In fact, the core of the Wasm specification has been formalised in the Isabelle proof assistant, as well as some of the metatheory. However, this does not cover the whole specification, and many other things can be built on top.

wasm_coq is an ongoing project to (1) replicate this effort in the Coq proof assistant, based on a need expressed by the Coq community, and (2) extend it to (a) cover more of the WebAssembly standard (so far, binary format parsing), (b) obtain a usable tool (so far, our tool can load, typecheck, and execute small Wasm binaries), and (c) build on top of it and connect it to other projects involving Wasm (separation logic, compilation to or from Wasm, ...).

Projects

The project would involve developing some aspect of the formalisation (to be discussed with the project supervisors): making the interpreter scale, validation, metatheory, connecting it to the Iris separation logic framework, etc.

Requirements

The student should have a good grasp or a strong willingness to learn the following topics:

The student should have a good grasp of the following topics:

Depending on the specifics of the project, the student should have a good grasp of some of the following topics:

Project supervisors

Jean Pichon-Pharabod and Neel Krishnaswami

(email jp622 to talk to if interested)

References

Mechanising proofs of equivalence of different formalisations of the x86-TSO relaxed memory models

MPhil/Part III (or motivated Part II) project

Context

x86-TSO is the memory model of concurrency on x86. It has a simple, well-understood characterisation in terms of an operational semantics where writes by a thread move through a FIFO buffer.

x86-TSO also has a characterisation in terms of an "axiomatic" memory model, that is, an acyclicity check over sets of unconstrained executions. This axiomatic memory model sheds a different light on the memory model, and lends itself well to bounded model checking.

Currently, we have pen-and-paper proofs of equivalence of the operational memory model and a version of the axiomatic memory model written in an old style.

Project

The core of the project would involve mechanising, in a proof assistant:

There are interesting opportunities to extend the models and proofs with extra features, like mixed-sized accesses, to generated executable code from the models that can be integrated into testing and exploration tools, to extract a bounded model-checker, connect it to other formalisations (dual TSO, ...), etc.

Requirements

The student should have a good grasp or a strong willingness to learn the following topics:

The student should have a good grasp of the following topics:

Project supervisors

Jean Pichon-Pharabod and Peter Sewell

(email jp622 to talk to if interested)

References

Last modified: 15 Oct 2020