diff --git a/CHANGELOG.md b/CHANGELOG.md index 27a81b79d4e4babb716e01ac1ad9f342f15745ac..3d7e8bc1bda7cd3cd533f1ccb04dfb8ae7b2c794 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -54,6 +54,12 @@ Changes in heap_lang: "normalized" to the same. This makes all closures indistinguishable from each other while remaining unqueal to anything else. We also use the same "normalization" to make sure all prophecy variables seem equal to `()`. +* CAS (compare-and-set) got replaced by CmpXchg (compare-exchange). The + difference is that CmpXchg returns a pair consisting of the old value and a + boolean indicating whether the comparison was successful and hence the + exchange happened. CAS can be obtained by simply projecting to the second + component, but also providing the old value more closely models the primitive + typically provided in systems languages (C, C++, Rust). Changes in Coq: