diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v index 09bec1ec5c30000c106d9d54ef879934cb46ca87..05a5dbdef2117d8efb8b31c16055bf70cce6d65d 100644 --- a/heap_lang/lib/lock.v +++ b/heap_lang/lib/lock.v @@ -5,7 +5,8 @@ Import uPred. Definition newlock : val := λ: <>, ref #false. Definition acquire : val := - rec: "lock" "l" := if: CAS '"l" #false #true then #() else '"lock" '"l". + rec: "acquire" "l" := + if: CAS '"l" #false #true then #() else '"acquire" '"l". Definition release : val := λ: "l", '"l" <- #false. (** The CMRA we need. *)