Initial commit

.github/workflows/main.yml

@@ -0,0 +1,20 @@
+name: CI
+
+on: [push]
+
+jobs:
+  build:
+
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v1
+    - name: Get TLAPS
+      run: wget https://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-1.4.5-x86_64-linux-gnu-inst.bin
+    - name: Install TLAPS
+      run: |
+        chmod +x tlaps-1.4.5-x86_64-linux-gnu-inst.bin
+        ./tlaps-1.4.5-x86_64-linux-gnu-inst.bin -d tlaps
+    - name: Run TLAPS
+      run: tlaps/bin/tlapm --cleanfp -I tlaps/ tlaplus/BlockingQueue.tla
+

CONTRIBUTING.md

@@ -0,0 +1,16 @@
+# Contributing Guidelines
+
+## Adding a blocking queue
+
+Check out the "tlaplus" folder for an example of what this all looks like.
+
+One folder per blocking queue, one blocking queue per folder. If you're the first person uploading for your proof language, name the folder after your method. If someone else already submitted a proof, you should postpend your folder with what makes your proof special.
+
+Your code should formally prove the total specification of the blocking queue. It must do this without any assumptions in the proof, and the proof must correct. Proving intermediate lemmas or ghost functions is fine, as are using already-proven primitives your language's standard library.
+
+Along with your blocking queue, you should include a `readme.md` file. It should contain:
+* The name of your tool, and a link to learn more about it.
+* A description of the language. What does it look like? How does it work? What makes it different or special?
+* A description of your proof. How does it work? What interesting language properties or verification techniques does it showcase?
+
+That's pretty much it!

LICENSE

@@ -0,0 +1,121 @@
+Creative Commons Legal Code
+
+CC0 1.0 Universal
+
+    CREATIVE COMMONS CORPORATION IS NOT A LAW FIRM AND DOES NOT PROVIDE
+    LEGAL SERVICES. DISTRIBUTION OF THIS DOCUMENT DOES NOT CREATE AN
+    ATTORNEY-CLIENT RELATIONSHIP. CREATIVE COMMONS PROVIDES THIS
+    INFORMATION ON AN "AS-IS" BASIS. CREATIVE COMMONS MAKES NO WARRANTIES
+    REGARDING THE USE OF THIS DOCUMENT OR THE INFORMATION OR WORKS
+    PROVIDED HEREUNDER, AND DISCLAIMS LIABILITY FOR DAMAGES RESULTING FROM
+    THE USE OF THIS DOCUMENT OR THE INFORMATION OR WORKS PROVIDED
+    HEREUNDER.
+
+Statement of Purpose
+
+The laws of most jurisdictions throughout the world automatically confer
+exclusive Copyright and Related Rights (defined below) upon the creator
+and subsequent owner(s) (each and all, an "owner") of an original work of
+authorship and/or a database (each, a "Work").
+
+Certain owners wish to permanently relinquish those rights to a Work for
+the purpose of contributing to a commons of creative, cultural and
+scientific works ("Commons") that the public can reliably and without fear
+of later claims of infringement build upon, modify, incorporate in other
+works, reuse and redistribute as freely as possible in any form whatsoever
+and for any purposes, including without limitation commercial purposes.
+These owners may contribute to the Commons to promote the ideal of a free
+culture and the further production of creative, cultural and scientific
+works, or to gain reputation or greater distribution for their Work in
+part through the use and efforts of others.
+
+For these and/or other purposes and motivations, and without any
+expectation of additional consideration or compensation, the person
+associating CC0 with a Work (the "Affirmer"), to the extent that he or she
+is an owner of Copyright and Related Rights in the Work, voluntarily
+elects to apply CC0 to the Work and publicly distribute the Work under its
+terms, with knowledge of his or her Copyright and Related Rights in the
+Work and the meaning and intended legal effect of CC0 on those rights.
+
+1. Copyright and Related Rights. A Work made available under CC0 may be
+protected by copyright and related or neighboring rights ("Copyright and
+Related Rights"). Copyright and Related Rights include, but are not
+limited to, the following:
+
+  i. the right to reproduce, adapt, distribute, perform, display,
+     communicate, and translate a Work;
+ ii. moral rights retained by the original author(s) and/or performer(s);
+iii. publicity and privacy rights pertaining to a person's image or
+     likeness depicted in a Work;
+ iv. rights protecting against unfair competition in regards to a Work,
+     subject to the limitations in paragraph 4(a), below;
+  v. rights protecting the extraction, dissemination, use and reuse of data
+     in a Work;
+ vi. database rights (such as those arising under Directive 96/9/EC of the
+     European Parliament and of the Council of 11 March 1996 on the legal
+     protection of databases, and under any national implementation
+     thereof, including any amended or successor version of such
+     directive); and
+vii. other similar, equivalent or corresponding rights throughout the
+     world based on applicable law or treaty, and any national
+     implementations thereof.
+
+2. Waiver. To the greatest extent permitted by, but not in contravention
+of, applicable law, Affirmer hereby overtly, fully, permanently,
+irrevocably and unconditionally waives, abandons, and surrenders all of
+Affirmer's Copyright and Related Rights and associated claims and causes
+of action, whether now known or unknown (including existing as well as
+future claims and causes of action), in the Work (i) in all territories
+worldwide, (ii) for the maximum duration provided by applicable law or
+treaty (including future time extensions), (iii) in any current or future
+medium and for any number of copies, and (iv) for any purpose whatsoever,
+including without limitation commercial, advertising or promotional
+purposes (the "Waiver"). Affirmer makes the Waiver for the benefit of each
+member of the public at large and to the detriment of Affirmer's heirs and
+successors, fully intending that such Waiver shall not be subject to
+revocation, rescission, cancellation, termination, or any other legal or
+equitable action to disrupt the quiet enjoyment of the Work by the public
+as contemplated by Affirmer's express Statement of Purpose.
+
+3. Public License Fallback. Should any part of the Waiver for any reason
+be judged legally invalid or ineffective under applicable law, then the
+Waiver shall be preserved to the maximum extent permitted taking into
+account Affirmer's express Statement of Purpose. In addition, to the
+extent the Waiver is so judged Affirmer hereby grants to each affected
+person a royalty-free, non transferable, non sublicensable, non exclusive,
+irrevocable and unconditional license to exercise Affirmer's Copyright and
+Related Rights in the Work (i) in all territories worldwide, (ii) for the
+maximum duration provided by applicable law or treaty (including future
+time extensions), (iii) in any current or future medium and for any number
+of copies, and (iv) for any purpose whatsoever, including without
+limitation commercial, advertising or promotional purposes (the
+"License"). The License shall be deemed effective as of the date CC0 was
+applied by Affirmer to the Work. Should any part of the License for any
+reason be judged legally invalid or ineffective under applicable law, such
+partial invalidity or ineffectiveness shall not invalidate the remainder
+of the License, and in such case Affirmer hereby affirms that he or she
+will not (i) exercise any of his or her remaining Copyright and Related
+Rights in the Work or (ii) assert any associated claims and causes of
+action with respect to the Work, in either case contrary to Affirmer's
+express Statement of Purpose.
+
+4. Limitations and Disclaimers.
+
+ a. No trademark or patent rights held by Affirmer are waived, abandoned,
+    surrendered, licensed or otherwise affected by this document.
+ b. Affirmer offers the Work as-is and makes no representations or
+    warranties of any kind concerning the Work, express, implied,
+    statutory or otherwise, including without limitation warranties of
+    title, merchantability, fitness for a particular purpose, non
+    infringement, or the absence of latent or other defects, accuracy, or
+    the present or absence of errors, whether or not discoverable, all to
+    the greatest extent permissible under applicable law.
+ c. Affirmer disclaims responsibility for clearing rights of other persons
+    that may apply to the Work or any use thereof, including without
+    limitation any person's Copyright and Related Rights in the Work.
+    Further, Affirmer disclaims responsibility for obtaining any necessary
+    consents, permissions or other rights required for any use of the
+    Work.
+ d. Affirmer understands and acknowledges that Creative Commons is not a
+    party to this document and has no duty or obligation with respect to
+    this CC0 or use of the Work.

README.md

@@ -0,0 +1,88 @@
+# Let's prove a blocking queue deadlock-free
+
+This is a repository of provably deadlock-free blocking queue.
+
+This challenge was inspired by [lets-prove-leftpad](https://github.com/hwayne/lets-prove-leftpad) (from which this README and the contribution guide have been adopted).  However, while lets-prove-leftpad is about a sequential algorithm, this challenge is about a concurrent one.
+
+## What is "provably-correct"?
+
+**Provably correct** is a guarantee that an algorithm satisfies given correctness properties, say deadlock freedom. You do this by providing a **proof** that a computer can check. If the proof is wrong, the computer will tell you that your algorithm is incorrect (wrt correctness properties). Or as Donald Knuth puts it: "[Beware of bugs in the above code; I have only proved it correct, not tried it.](https://www-cs-faculty.stanford.edu/~knuth/faq.html)" 
+
+Compare to something like testing: even if you run your test for days and days, you still don't know _for sure_ that keeping it running for another minute won't reveal a deadlock. With a proof, though, you know your algorithm will be deadlock-free after a computer has verified the proof. Proving correctness is really, really powerful. It's also [time consuming](https://xavierleroy.org/talks/IHP-2014.pdf) and often not worth the effort.
+
+This is a sampler of all the different tools we can use to prove algorithms and (implementations) correct, standardized by all being proofs for a simple concurrent data-structure most likely every programmer has encountered in her career.
+
+## What is a "blocking queue"?
+
+A [queue](https://en.wikipedia.org/wiki/Queue_(abstract_data_type)) that blocks until the queue becomes non-empty when consumers retrieve an element, and waits for space to become available when producers store an element. The queue has a fixed/static capacity. For simplicity, we will only consider finite and disjoint sets of producers and consumers. In other words, a producer is blocked if the queue is full; a consumer is blocked if it's empty.
+
+The task is to prove that your blocking queue is guaranteed to never deadlock no matter the queue's capacity, the number of producers, or the number of consumers in the system. If there is space in the queue, some producer will eventually add an element to the queue. If there are elements in the queue, some consumer will eventually remove them from the queue.  More formally: Let P and C be the sets of the producer and consumer threads and let W be the set of all waiting/sleeping/blocked threads. Prove that ```(P \cup C) # W``` is a valid property of your blocking queue.
+
+Since C is perhaps common ground for most of us, below is a listing of a blocking queue implementation:
+
+```C
+#include <stdio.h>
+#include <stdlib.h>
+#include <stdint.h>
+#include <pthread.h>
+
+uint32_t buff_size;
+uint32_t *buffer;
+uint32_t fillIndex, useIndex, count = 0;
+
+pthread_cond_t empty, full; 
+pthread_mutex_t mutex;
+
+void put(uint32_t value) {
+	buffer[fillIndex] = value;
+	fillIndex = (fillIndex + 1) % buff_size;
+	count++;
+}
+
+uint32_t get() {
+	uint32_t tmp = buffer[useIndex];
+	useIndex = (useIndex + 1) % buff_size;
+	count--;
+	return tmp;
+}
+
+void *producer (void * arg) {
+	while(1) {
+		pthread_mutex_lock(&mutex);
+
+		while (count == buff_size)
+			pthread_cond_wait(&empty, &mutex);
+
+		put(rand() % 10);
+
+		pthread_cond_signal(&full);
+		pthread_mutex_unlock(&mutex);
+	}
+}
+
+void *consumer (void * arg) {
+	while(1) {
+		pthread_mutex_lock(&mutex);
+
+		while (count == 0)
+			pthread_cond_wait(&full, &mutex);
+
+		get();
+
+		pthread_cond_signal(&empty);
+		pthread_mutex_unlock(&mutex);
+	} 
+}
+
+...
+```
+
+## Why are we proving deadlock freedom?
+
+It is a great demo for different proof techniques. The idea is simple, but the algorithm (and implementations) is easy to get wrong.  The concept of concurrency is challenging for humans to get right. However, the demise of Moore's law means that algorithms have to become concurrent to keep up with growing workloads. Thus, verification pays off in this area, especially so because concurrency bugs tend to manifest in unexpected/unpredictable behavior.
+
+A proof of deadlock-freedom is going to be small enough to be (mostly) grokkable by Formal Methods outsiders, while being complex enough to differentiate the ways we prove code correct.
+
+## I want to contribute!
+
+We'd love to have you! Please [read the contribution guidelines](CONTRIBUTING.md) and then submit your favorite proofs!

tlaplus/BlockingQueue.tla

@@ -0,0 +1,83 @@
+-------------------- MODULE BlockingQueue -----------------------
+EXTENDS Naturals, Sequences, TLAPS
+
+CONSTANTS Producers, Consumers, BufCapacity
+
+ASSUME Assumptions == /\ Producers # {} /\ Consumers # {}
+                      /\ (Consumers \intersect Producers) = {}
+                      /\ BufCapacity \in (Nat \ {0})
+
+data == CHOOSE d : d \* Some data.
+
+-----------------------------------------------------------------
+
+VARIABLES buffer, waitC, waitP
+vars == <<buffer, waitC, waitP>>
+
+TypeOK == /\ Len(buffer) \in 0..BufCapacity
+          /\ waitP \in SUBSET Producers
+          /\ waitC \in SUBSET Consumers
+
+NoDeadlock == (waitC \cup waitP) # (Producers \cup Consumers)
+
+Notify(ws) == IF ws # {}
+              THEN \E x \in ws: ws' = ws \ {x}
+              ELSE UNCHANGED ws
+
+Wait(ws, t) == /\ ws' = ws \cup {t}
+               /\ UNCHANGED buffer
+
+Put(t, d) == \/ /\ Len(buffer) < BufCapacity
+                /\ buffer' = Append(buffer, d)
+                /\ Notify(waitC) /\ UNCHANGED waitP
+             \/ /\ Len(buffer) = BufCapacity
+                /\ Wait(waitP, t) /\ UNCHANGED waitC
+
+Get(t) == \/ /\ buffer # <<>>
+             /\ buffer' = Tail(buffer)
+             /\ Notify(waitP) /\ UNCHANGED waitC
+          \/ /\ buffer = <<>>
+             /\ Wait(waitC, t) /\ UNCHANGED waitP
+
+Init == buffer = <<>> /\ waitC = {} /\ waitP = {}
+
+Next == \/ \E t \in (Producers \ waitP): Put(t, data)
+        \/ \E t \in (Consumers \ waitC): Get(t)
+
+Spec == Init /\ [][Next]_vars
+
+-----------------------------------------------------------------
+
+(* Scaffolding: Establish that TypeOK is inductive. *)
+LEMMA ITypeInv == Spec => []TypeOK
+<1> USE Assumptions DEF TypeOK
+<1>1. Init => TypeOK 
+   BY DEF Init
+<1>2. TypeOK /\ [Next]_vars => TypeOK'  
+  BY DEF Next, vars, Put, Get, Notify, Wait
+<1>. QED BY <1>1, <1>2, PTL DEF Spec
+
+-----------------------------------------------------------------
+
+(* An inductive invariant that implies NoDeadlock. *)
+IInv == /\ TypeOK
+        /\ NoDeadlock
+        (* This is the meat! *)
+        /\ buffer = <<>> => (Producers \ waitP) # {}
+        /\ Len(buffer) = BufCapacity => (Consumers \ waitC) # {}
+
+-----------------------------------------------------------------
+
+(* Proof that Spec is deadlock-free. *)
+THEOREM DeadlockFreedom == Spec => []IInv
+<1> USE Assumptions DEF IInv, NoDeadlock, TypeOK
+<1>1. Init => IInv
+  BY DEF Init
+<1>2. IInv /\ [Next]_vars => IInv' 
+  BY DEF Next, vars, Put, Get, Notify, Wait
+<1>3. IInv => NoDeadlock
+  BY DEF IInv
+<1>4. QED
+  BY <1>1,<1>2,<1>3,PTL DEF Spec
+
+=================================================================