cspec

public

12 stars

1 forks

0 issues

Commits

List of commits on branch master.

Unverified

04bce7a9f7429fa305199e7542fc6e33f20e0899

Update stack to latest resolver

ttchajed committed 6 years ago

Unverified

76e6ed7bece5e33240fa456e341a2e1e823b421e

Fix coqdoc call in Makefile

ttchajed committed 6 years ago

Unverified

54391d79f0e05b4b02a5aadd27c3ad193bfcad97

Fix compatibility issues with Coq master

ttchajed committed 6 years ago

Unverified

48234d38fb4467f03b34c52d392d92c0de7ffdf1

Temporarily ignore no implicit hintdb warning

ttchajed committed 6 years ago

Unverified

28dc02b73c44a82c0e8f8d1b1459613840b2982c

checkpoint start of a brute-force proof

zzeldovich committed 6 years ago

Unverified

7ac01d690c87da1726aa5d94e2f9831df6d78a7f

checkpoint some more thoughts on an atomic counter client API

zzeldovich committed 6 years ago

README

The README file for this repository.

CSPEC

Framework for reasoning about concurrent code using abstraction, layers, and movers.

Compiling

You'll need Coq v8.9 or master, Go, and Haskell stack.

To compile CSPEC, CMAIL, and GoMail, run make. A benchmarking binary for CMAIL is output to bin/mail-test and a GoMail binary that listens for SMTP and POP3 connections is output to bin/gomail.

The stack initialization doesn't handle parallel builds correctly so a parallel build with a fresh stack install may not work, but re-running should fix any concurrency issues (isn't that ironic?).