# 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.

Note

Why is it called Pulse? Because it grew from a prior logic called Steel, and one of the authors and his daughter are big fans of a classic reggae band called Steel Pulse. We wanted a name that was softer than Steel, and, well, a bit playful. So, Pulse!

- Getting up and running with Codespaces
- Pulse Basics
- Mutable References
- Existential Quantification
- User-defined Predicates
- Conditionals
- Loops & Recursion
- Mutable Arrays
- Ghost Computations
- Higher Order Functions
- Implication and Universal Quantification
- Linked Lists
- Atomic Operations and Invariants
- Spin Locks
- Parallel Increment
- Extraction