Adding more details in READMEs

Signed-off-by: JarodDif <jarod.differdange@gmail.com>

Author: JarodDif

specifications/barriers/README.md

@@ -1,5 +1,13 @@
 # Barrier synchronization
 
+A barrier is a synchronization facility which ensures that a group of threads
+all reach the barrier before they can advance.
+
+Such a barrier is useful when parallel computations are done in two or more
+steps and results from all threads are needed to continue.
+
+[Wikipedia](https://en.wikipedia.org/wiki/Barrier_(computer_science))
+
 ## Barrier.tla
 
 A specification of an abstract Barrier.
@@ -42,6 +50,3 @@ provided.
 ## Refinement
 
 A refinement towards an abstract Barrier specification is proven with TLAPS.
-
-A model `MCBarriers.cfg` and its companion `MCBarriers.tla` verifies if
-`B!Spec` (the abstract Barrier specification) holds for `Spec` 

specifications/locks_auxiliary_vars/README.md

@@ -18,10 +18,15 @@ In this abstract lock, lock acquisition is done atomically.
 
 ## Peterson.tla
 
-The specification of Peterson's algorithm in PlusCal, and the refinement proof
-towards `Lock!Spec`.
+Peterson's algorithm is a solution for mutual exclusion for 2 processes.
+Each process shows its intent to enter the critical section by raising a flag
+`c[self]` and can proceed if the other process does not intend to enter the 
+critical section or it is its turn.
 
-The refinement can be verified with TLC with `MCPeterson.tla/cfg`.
+[Wikipedia](https://en.wikipedia.org/wiki/Peterson%27s_algorithm)
+
+This module contains the specification of Peterson's algorithm in PlusCal, and 
+the refinement proof towards `Lock!Spec`.
 
 ## LockHS.tla
 
@@ -36,8 +41,6 @@ to allow a refinement towards Peterson's algorithm.
 
 A refinement proof towards `Peterson!Spec` is presented within.
 
-The refinement can be verified with TLC with `MCLockHS.tla/cfg`. 
-
 ## Stuttering.tla
 
 This module was written for the **Auxiliary variables in TLA+** paper by