Pulse: Proof-oriented Programming in Concurrent Separation Logic

Many F* projects involve building domain-specific languages with specialized programming and proving support. For example, Vale supports program proofs for a structured assembly language; Low* provides effectful programming in F* with a C-like memory model; EverParse is a DSL for writing low-level parsers and serializers. Recently, F* has gained new features for building DSLs embedded in F* with customized syntax, type checker plugins, extraction support, etc., with Pulse as a showcase example of such a DSL.

Pulse is a new programming language embedded in F*, inheriting many of its features (notably, it is higher order and has dependent types), but with built-in support for programming with mutable state and concurrency, with specifications and proofs in Concurrent Separation Logic.

As a first taste of Pulse, here’s a function to increment a mutable integer reference.

fn incr (x:ref int)
requires pts_to x 'i
ensures pts_to x ('i + 1)
{
    let v = !x;
    x := v + 1;
}

And here’s a function to increment two references in parallel.

fn par_incr (x y:ref int)
requires pts_to x 'i ** pts_to y 'j
ensures pts_to x ('i + 1) ** pts_to y ('j + 1)
{
   par (fun _ -> incr x)
       (fun _ -> incr y)
}

You may not have heard about separation logic before—but perhaps these specifications already make intuitive sense to you. The type of incr says that if “x points to ‘i” initially, then when incr returns, “x points to ‘i + 1”; while par_incr increments the contents of x and y in parallel by using the par combinator.

Concurrent separation logic is an active research area and there are many such logics out there, all with different tradeoffs. Pulse’s logic is based on a logic called PulseCore, formalized entirely within F*—you can find the formalization here. Proofs of programs in Pulse’s surface language correspond to proofs of correctness in the PulseCore program logic. But, you should not need to know much about how the logic is formalized to use Pulse effectively. We’ll start from the basics and explain what you need to know about concurrent separation logic to start programming and proving in Pulse. Additionally, Pulse is an extension of F*, so all you’ve learned about F*, lemmas, dependent types, refinement types, etc. will be of use again.