Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: lemmy/lets-prove-blocking-queue
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: master
Choose a base ref
...
head repository: franck44/lets-prove-blocking-queue
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: master
Choose a head ref
Able to merge. These branches can be automatically merged.
  • 1 commit
  • 2 files changed
  • 1 contributor

Commits on Apr 2, 2020

  1. Add Dafny spec and proof.

    franck44 committed Apr 2, 2020
    Copy the full SHA
    f84b3f5 View commit details
Showing with 171 additions and 0 deletions.
  1. +25 −0 dafny/README.md
  2. +146 −0 dafny/prod-cons.dfy
25 changes: 25 additions & 0 deletions dafny/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@

# Dafny

We use the verification-aware programming language Dafny to write the specification, the implementation, and the proofs.

Dafny provides extensive support for automated reasoning leveraging the power of state-of-start
automated reasonign engines (SMT-solvers).


# Useful Repositories - Dafny

* [Dafny github repo](https://github.com/dafny-lang/dafny)

* [Dafny Wiki](https://github.com/dafny-lang/dafny/wiki)

* [VSCode](https://code.visualstudio.com), to use Dafny on MacOS and Linux

* [Dafny-extension-for-VSCode](https://marketplace.visualstudio.com/items?itemName=correctnessLab.dafny-vscode)

* [Verification Corner](https://www.youtube.com/channel/UCP2eLEql4tROYmIYm5mA27A), tutorials by Rustan Leino.

* [Tutorial paper](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml220.pdf)

* [IronClad project (2015, Dafny spec)](https://github.com/Microsoft/Ironclad/tree/master/ironfleet)

146 changes: 146 additions & 0 deletions dafny/prod-cons.dfy
Original file line number Diff line number Diff line change
@@ -0,0 +1,146 @@
/**
* A proof in Dafny of the non blocking property of a queue.
* @author Franck Cassez.
*
* @note: based off Modelling Concurrency in Dafny, K.R.M. Leino
* @link{http://leino.science/papers/krml260.pdf}
*/
module ProdCons {

// A type for process id that supports equality (i.e. p == q is defined).
type Process(==)

// A type for the elemets in the buffer.
type T

/**
* The producer/consumer problem.
* The set of processes is actuall irrelevant (included here because part of the
* original problem statement ...)
*/
class ProdCons {

/**
* Set of processes in the system.
*/
const P: set<Process>

/**
* The maximal size of the buffer.
*/
var maxBufferSize : nat

/**
* The buffer.
*/
var buffer : seq<T>

/**
* Invariant.
*
* Buffer should always less than maxBufferSize elements,
* Set of processes is not empty
*
*/
predicate valid()
reads this
{
maxBufferSize > 0 && P != {} &&
0 <= |buffer| <= maxBufferSize
}

/**
* Initialise set of processes and buffer and maxBufferSize
*/
constructor (processes: set<Process>, m: nat )
requires processes != {} // Non empty set of processes.
requires m >= 1 // Buffer as at least one cell.
ensures valid() // After initilisation the invariant is true
{
P := processes;
buffer := [];
maxBufferSize := m;
}

/**
* Enabledness of a put operation.
* If enabled any process can perform a put.
*/
predicate putEnabled(p : Process)
reads this
{
|buffer| < maxBufferSize
}

/** Event: a process puts an element in the queue. */
method put(p: Process, t : T)
requires valid()
requires putEnabled(p) // |buffer| < maxBufferSize
modifies this
{
buffer := buffer + [t] ;
}

/**
* Enabledness of a get operation.
* If enabled, any process can perform a get.
*/
predicate getEnabled(p : Process)
reads this
{
|buffer| >= 1
}

/** Event: a process gets an element from the queue. */
method get(p: Process)
requires getEnabled(p)
requires valid() // Invariant is inductive
ensures |buffer| == |old(buffer)| - 1 // this invariant is not needed and can be omitted
modifies this
{
// remove the first element of buffer.
// note: Dafny implcitly proves that the tail operation can be performed
// as a consequence of |buffer| >= 1 (getEnabled()).
// To see this, comment out the
// requires and an error shows up.
buffer := buffer[1..];
}

/** Correctness theorem: no deadlock.
* From any valid state, at least one process is enabled.
*/
lemma noDeadlock()
requires valid()
ensures exists p :: p in P && (getEnabled(p) || putEnabled(p))

// as processes are irrelevant, this could be simplified
// into isBufferNotFull() or isBufferNotEmpty()
{
// Dafny automatically proves this. so we can leave the
// body of this lemma empty.
// But for the sake of clarity, here is the proof.

// P is not empty so there is a process p in P
// Reads as: select a p of type Process such that p in P
var p: Process :| p in P ;
// Now we have a p.
// We are going to use the fact that valid() must hold as it is a pre-condition
if ( |buffer| > 0 ) {
assert (getEnabled(p));
}
else {
// You may comment out the following asserts and Dafny
// can figure out the proof from the constraints that are
// true in this case.
// Becas=use |buffer| == 0 and maxBufferSize >= 1, we can do a put
assert(|buffer| == 0);
assert (|buffer| < maxBufferSize);
assert(putEnabled(p));
}
}
}
}