From efa4a5df14ae89c1b6d6a1aec72f478922ed34a0 Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Thu, 9 Nov 2017 13:35:17 +0100
Subject: [PATCH] Update CHANGELOG.md.

---
 CHANGELOG.md | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a3305d696..71bcaac71 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -13,6 +13,13 @@ Changes in and extensions of the theory:
 * Constructions for least and greatest fixed points over monotone predicates
   (defined in the logic of Iris using impredicative quantification).
 * Add a proof of the inverse of `wp_bind`.
+* Support verifying code that might get stuck by distinguishing
+  "progressive" vs. "non-progressive" weakest preconditions. (See
+  [Swasey et al. OOPSLA '17] for examples.) The progressive `WP e @ E
+  {{ Φ }}` ensures that, as `e` runs, it does not get stuck. The
+  non-progressive `WP e @ E ?{{ Φ }}` ensures that, as usual, all
+  invariants are preserved while `e` runs, but it permits execution to
+  get stuck. The former implies the latter.
 
 Changes in Coq:
 
@@ -88,6 +95,13 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
 * Move the `prelude` folder to its own project: std++
 * The rules `internal_eq_rewrite` and `internal_eq_rewrite_contractive` are now
   stated in the logic, i.e. they are `iApply` friendly.
+* Use *stuckness bits* `s` to define progressive vs. non-progressive
+  WP. The full judgment is `WP e @ s; E {{ Φ }}`; progressive WP uses
+  `s = not_stuck` while non-progressive WP uses `s = maybe_stuck`.
+* Restore the original, stronger notion of atomicity alongside the
+  weaker notion. These are `Atomic s e` where the stuckness bit `s`
+  indicates whether expression `e` is weakly (`s = not_stuck`) or
+  strongly (`s = maybe_stuck`) atomic.
 
 ## Iris 3.0.0 (released 2017-01-11)
 
-- 
GitLab