Habanero Phaser formalization

Phaser state operations

Welcome to our online interpreter of the Habanero formalization. Read on the developer notes for information about the implementation of this page.

The following two operations are translated automatically from our Coq formalization into Javascript.

• hj.run(op,ph) performs a reduction step by applying operation op to phaser state ph. The function returns the new state or throws an exception if it cannot reduce.
• hj.hb(ph1,ph2) returns true if, and only if, phaser ph1 happened before phaser ph2.
• hj.par(ph1,ph2) returns true if, and only if, phaser ph1 may happen in parallel with ph2.
• hj.wf(ph) returns true if, and only if, phaser ph is well-formed.
• hj.wo(ph) returns true if, and only if, phaser ph is well-ordered.

Executable samples. The widget below is a Javascript REPL; input a Javascript expression to exercise our functions.

Happens-before visualization

The trace in the text box is rendered as a graph. Editing the trace automatically updates the graph.

Rendering of the trace:

Trace manipulation

We provide the following functions to handle a trace:

• trace() returns the trace from the input text box.
• hj.run_trace(t) returns a phaser state from a given trace t.
• hj.render_graph(t) renders trace t in the visualization widget.

Colophon

• Web page
• Coq formalization and Javascript library

• Coq
• OCaml
• js_of_ocaml
• js sandbox console
• vis.js