From d59fec71cbdb54a0a48445c8017d761100e3865e Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 22 Oct 2024 07:56:19 -0700 Subject: [PATCH] [Civl] Added shared vector sample (#971) --- Test/civl/large-samples/shared-vector.bpl | 336 ++++++++++++++++++ .../large-samples/shared-vector.bpl.expect | 2 + .../treiber-stack.bpl | 0 .../treiber-stack.bpl.expect | 0 4 files changed, 338 insertions(+) create mode 100644 Test/civl/large-samples/shared-vector.bpl create mode 100644 Test/civl/large-samples/shared-vector.bpl.expect rename Test/civl/{samples => large-samples}/treiber-stack.bpl (100%) rename Test/civl/{samples => large-samples}/treiber-stack.bpl.expect (100%) diff --git a/Test/civl/large-samples/shared-vector.bpl b/Test/civl/large-samples/shared-vector.bpl new file mode 100644 index 000000000..1c9e2cb6b --- /dev/null +++ b/Test/civl/large-samples/shared-vector.bpl @@ -0,0 +1,336 @@ +// RUN: %parallel-boogie -timeLimit:0 -vcsSplitOnEveryAssert "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +//////////////////////////////////////////////////////////////////////////////// +// Shared integer array implementation + +var {:layer 9, 100} IntArrayPool: Map Loc (Vec int); + +datatype IntArray { + IntArray( + {:linear "no_collect_keys"} mutexes: Map int (One Loc), + {:linear "no_collect_keys"} values: Map int (Cell Loc int) + ) +} + +var {:layer 0, 9} {:linear} IntArrayPoolLow: Map Loc IntArray; + +yield invariant {:layer 9} IntArrayDom(); +invariant IntArrayPool->dom == IntArrayPoolLow->dom; + +yield invariant {:layer 9} Yield(loc_iv: Loc); +invariant Map_Contains(IntArrayPoolLow, loc_iv); +invariant + (var intvec_low, intvec_high := Map_At(IntArrayPoolLow, loc_iv), Map_At(IntArrayPool, loc_iv); + intvec_low->mutexes->dom == intvec_low->values->dom && + intvec_low->mutexes->dom->val == (lambda i: int :: 0 <= i && i < Vec_Len(intvec_high)) && + (forall j: int:: 0 <= j && j < Vec_Len(intvec_high) ==> Map_Contains(MutexPool, Map_At(intvec_low->mutexes, j)->val)) && + (forall j: int:: 0 <= j && j < Vec_Len(intvec_high) ==> Map_At(intvec_low->values, j)->val == Vec_Nth(intvec_high, j))); + + +atomic action {:layer 10, 100} Atomic_IntArray_Alloc(v: Vec int) returns (loc_iv: Loc) +modifies IntArrayPool; +{ + var {:linear} one_loc_iv: One Loc; + call one_loc_iv := Loc_New(); + loc_iv := one_loc_iv->val; + assume !Map_Contains(IntArrayPool, loc_iv); + IntArrayPool := Map_Update(IntArrayPool, loc_iv, v); +} +yield procedure {:layer 9} IntArray_Alloc(v: Vec int) returns (loc_iv: Loc) +refines Atomic_IntArray_Alloc; +preserves call IntArrayDom(); +{ + var {:linear} one_loc_mutex: One Loc; + var {:linear} cell_int: Cell Loc int; + var {:linear "no_collect_keys"} mutexes: Map int (One Loc); + var {:linear "no_collect_keys"} values: Map int (Cell Loc int); + var {:linear} intvec: IntArray; + var i: int; + var {:linear} one_loc_i: One Loc; + var {:linear} one_loc_iv: One Loc; + var {:layer 9} OldMutexPool: Map Loc Mutex; + + call mutexes := Map_MakeEmpty(); + call values := Map_MakeEmpty(); + + call {:layer 9} OldMutexPool := Copy(MutexPool); + i := 0; + while (i < Vec_Len(v)) + invariant {:layer 9} 0 <= i; + invariant {:layer 9} mutexes->dom == values->dom; + invariant {:layer 9} mutexes->dom->val == (lambda j: int :: 0 <= j && j < i); + invariant {:layer 9} (forall j: int:: 0 <= j && j < i ==> Map_Contains(MutexPool, Map_At(mutexes, j)->val)); + invariant {:layer 9} (forall j: int:: 0 <= j && j < i ==> Map_At(values, j)->val == Vec_Nth(v, j)); + invariant {:layer 9} Set_IsSubset(OldMutexPool->dom, MutexPool->dom); + { + call one_loc_mutex := Mutex_Alloc(); + call Map_PutValue(mutexes, i, one_loc_mutex); + call one_loc_i := Loc_New(); + cell_int := Cell(one_loc_i, Vec_Nth(v, i)); + call Map_PutValue(values, i, cell_int); + i := i + 1; + } + + intvec := IntArray(mutexes, values); + call one_loc_iv := Loc_New(); + loc_iv := one_loc_iv->val; + call AddIntArrayToPool(one_loc_iv, intvec); + call {:layer 9} IntArrayPool := Copy(Map_Update(IntArrayPool, one_loc_iv->val, v)); +} + +atomic action {:layer 10, 100} Atomic_IntArray_Read({:linear} tid: One Tid, loc_iv: Loc, i: int) returns (v: int) +{ + var vec: Vec int; + assert Map_Contains(IntArrayPool, loc_iv); + vec := Map_At(IntArrayPool, loc_iv); + assert Vec_Contains(vec, i); + v := Vec_Nth(vec, i); +} +yield procedure {:layer 9} IntArray_Read({:linear} tid: One Tid, loc_iv: Loc, i: int) returns (v: int) +refines Atomic_IntArray_Read; +preserves call IntArrayDom(); +preserves call Yield(loc_iv); +{ + var loc_mutex: Loc; + var {:linear} cell_int: Cell Loc int; + var {:linear} one_loc_int: One Loc; + + call loc_mutex := GetLocMutex(loc_iv, i); + call Mutex_Acquire(tid, loc_mutex); + call cell_int := Locked_GetOwnedLocInt(tid, loc_iv, i); + Cell(one_loc_int, v) := cell_int; + cell_int := Cell(one_loc_int, v); + call Locked_PutOwnedLocInt(tid, loc_iv, i, cell_int); + call Mutex_Release(tid, loc_mutex); +} + +atomic action {:layer 10, 100} Atomic_IntArray_Write({:linear} tid: One Tid, loc_iv: Loc, i: int, v: int) +modifies IntArrayPool; +{ + var vec: Vec int; + assert Map_Contains(IntArrayPool, loc_iv); + vec := Map_At(IntArrayPool, loc_iv); + assert Vec_Contains(vec, i); + vec := Vec_Update(vec, i, v); + IntArrayPool := Map_Update(IntArrayPool, loc_iv, vec); +} +yield procedure {:layer 9} IntArray_Write({:linear} tid: One Tid, loc_iv: Loc, i: int, v: int) +refines Atomic_IntArray_Write; +preserves call IntArrayDom(); +preserves call Yield(loc_iv); +{ + var loc_mutex: Loc; + var {:linear} cell_int: Cell Loc int; + var {:linear} one_loc_int: One Loc; + var v': int; + + call loc_mutex := GetLocMutex(loc_iv, i); + call Mutex_Acquire(tid, loc_mutex); + call cell_int := Locked_GetOwnedLocInt(tid, loc_iv, i); + Cell(one_loc_int, v') := cell_int; + cell_int := Cell(one_loc_int, v); + call Locked_PutOwnedLocInt(tid, loc_iv, i, cell_int); + call Mutex_Release(tid, loc_mutex); + call {:layer 9} IntArrayPool := Copy(Map_Update(IntArrayPool, loc_iv, Vec_Update(Map_At(IntArrayPool, loc_iv), i, v))); +} + +atomic action {:layer 10, 100} Atomic_IntArray_Swap({:linear} tid: One Tid, loc_iv: Loc, i: int, j: int) +modifies IntArrayPool; +{ + var vec: Vec int; + assert Map_Contains(IntArrayPool, loc_iv); + vec := Map_At(IntArrayPool, loc_iv); + assert Vec_Contains(vec, i) && Vec_Contains(vec, j); + vec := Vec_Swap(vec, i, j); + IntArrayPool := Map_Update(IntArrayPool, loc_iv, vec); +} +yield procedure {:layer 9} IntArray_Swap({:linear} tid: One Tid, loc_iv: Loc, i: int, j: int) +refines Atomic_IntArray_Swap; +preserves call IntArrayDom(); +preserves call Yield(loc_iv); +{ + var loc_mutex_i: Loc; + var loc_mutex_j: Loc; + var loc_int_i: Loc; + var loc_int_j: Loc; + var ii: int; + var jj: int; + var i': int; + var j': int; + var {:linear} cell_int_i: Cell Loc int; + var {:linear} cell_int_j: Cell Loc int; + + if (i == j) { + return; + } + + // deadlock avoidance + if (i < j) { + ii := i; + jj := j; + } else { + ii := j; + jj := i; + } + + call loc_mutex_i := GetLocMutex(loc_iv, i); + call loc_mutex_j := GetLocMutex(loc_iv, j); + call Mutex_Acquire(tid, loc_mutex_i); + call Mutex_Acquire(tid, loc_mutex_j); + call cell_int_i := Locked_GetOwnedLocInt(tid, loc_iv, i); + call cell_int_j := Locked_GetOwnedLocInt(tid, loc_iv, j); + call Locked_PutOwnedLocInt(tid, loc_iv, i, cell_int_j); + call Locked_PutOwnedLocInt(tid, loc_iv, j, cell_int_i); + call Mutex_Release(tid, loc_mutex_j); + call Mutex_Release(tid, loc_mutex_i); + call {:layer 9} IntArrayPool := Copy(Map_Update(IntArrayPool, loc_iv, Vec_Swap(Map_At(IntArrayPool, loc_iv), i, j))); +} + +right action {:layer 1, 9} Atomic_GetLocMutex(loc_iv: Loc, i: int) returns (loc_mutex: Loc) +modifies IntArrayPoolLow; +{ + var {:linear} one_loc_iv: One Loc; + var {:linear} intvec: IntArray; + var {:linear "no_collect_keys"} mutexes: Map int (One Loc); + var {:linear "no_collect_keys"} values: Map int (Cell Loc int); + var {:linear} one_loc_mutex: One Loc; + + call one_loc_iv, intvec := Map_Get(IntArrayPoolLow, loc_iv); + IntArray(mutexes, values) := intvec; + call one_loc_mutex := Map_GetValue(mutexes, i); + loc_mutex := one_loc_mutex->val; + call Map_PutValue(mutexes, i, one_loc_mutex); + intvec := IntArray(mutexes, values); + call Map_Put(IntArrayPoolLow, one_loc_iv, intvec); +} +yield procedure {:layer 0} GetLocMutex(loc_iv: Loc, i: int) returns (loc_mutex: Loc); +refines Atomic_GetLocMutex; + +both action {:layer 2, 9} Atomic_Locked_GetOwnedLocInt({:linear} tid: One Tid, loc_iv: Loc, i: int) returns ({:linear} cell_int: Cell Loc int) +modifies IntArrayPoolLow; +{ + var {:linear} one_loc_iv: One Loc; + var {:linear} intvec: IntArray; + var {:linear "no_collect_keys"} mutexes: Map int (One Loc); + var {:linear "no_collect_keys"} values: Map int (Cell Loc int); + + call one_loc_iv, intvec := Map_Get(IntArrayPoolLow, loc_iv); + IntArray(mutexes, values) := intvec; + + // the following lines are added over Atomic_GetOwnedLocInt + assert Map_Contains(MutexPool, Map_At(mutexes, i)->val); + assert Map_At(MutexPool, Map_At(mutexes, i)->val) == Some(tid->val); + + call cell_int := Map_GetValue(values, i); + intvec := IntArray(mutexes, values); + call Map_Put(IntArrayPoolLow, one_loc_iv, intvec); +} +yield procedure {:layer 1} Locked_GetOwnedLocInt({:linear} tid: One Tid, loc_iv: Loc, i: int) returns ({:linear} cell_int: Cell Loc int) +refines Atomic_Locked_GetOwnedLocInt; +{ + call cell_int := GetOwnedLocInt(loc_iv, i); +} + +both action {:layer 2, 9} Atomic_Locked_PutOwnedLocInt({:linear} tid: One Tid, loc_iv: Loc, i: int, {:linear_in} cell_int: Cell Loc int) +modifies IntArrayPoolLow; +{ + var {:linear} one_loc_iv: One Loc; + var {:linear} intvec: IntArray; + var {:linear "no_collect_keys"} mutexes: Map int (One Loc); + var {:linear "no_collect_keys"} values: Map int (Cell Loc int); + + call one_loc_iv, intvec := Map_Get(IntArrayPoolLow, loc_iv); + IntArray(mutexes, values) := intvec; + + // the following lines are added over Atomic_PutOwnedLocInt + assert Map_Contains(MutexPool, Map_At(mutexes, i)->val); + assert Map_At(MutexPool, Map_At(mutexes, i)->val) == Some(tid->val); + + call Map_PutValue(values, i, cell_int); + intvec := IntArray(mutexes, values); + call Map_Put(IntArrayPoolLow, one_loc_iv, intvec); +} +yield procedure {:layer 1} Locked_PutOwnedLocInt({:linear} tid: One Tid, loc_iv: Loc, i: int, {:linear_in} cell_int: Cell Loc int) +refines Atomic_Locked_PutOwnedLocInt; +{ + call PutOwnedLocInt(loc_iv, i, cell_int); +} + +atomic action {:layer 1, 1} Atomic_GetOwnedLocInt(loc_iv: Loc, i: int) returns ({:linear} cell_int: Cell Loc int) +modifies IntArrayPoolLow; +{ + var {:linear} one_loc_iv: One Loc; + var {:linear} intvec: IntArray; + var {:linear "no_collect_keys"} mutexes: Map int (One Loc); + var {:linear "no_collect_keys"} values: Map int (Cell Loc int); + + call one_loc_iv, intvec := Map_Get(IntArrayPoolLow, loc_iv); + IntArray(mutexes, values) := intvec; + call cell_int := Map_GetValue(values, i); + intvec := IntArray(mutexes, values); + call Map_Put(IntArrayPoolLow, one_loc_iv, intvec); +} +yield procedure {:layer 0} GetOwnedLocInt(loc_iv: Loc, i: int) returns ({:linear} cell_int: Cell Loc int); +refines Atomic_GetOwnedLocInt; + +atomic action {:layer 1, 1} Atomic_PutOwnedLocInt(loc_iv: Loc, i: int, {:linear_in} cell_int: Cell Loc int) +modifies IntArrayPoolLow; +{ + var {:linear} one_loc_iv: One Loc; + var {:linear} intvec: IntArray; + var {:linear "no_collect_keys"} mutexes: Map int (One Loc); + var {:linear "no_collect_keys"} values: Map int (Cell Loc int); + + call one_loc_iv, intvec := Map_Get(IntArrayPoolLow, loc_iv); + IntArray(mutexes, values) := intvec; + call Map_PutValue(values, i, cell_int); + intvec := IntArray(mutexes, values); + call Map_Put(IntArrayPoolLow, one_loc_iv, intvec); +} +yield procedure {:layer 0} PutOwnedLocInt(loc_iv: Loc, i: int, {:linear_in} cell_int: Cell Loc int); +refines Atomic_PutOwnedLocInt; + +atomic action {:layer 1, 9} Atomic_AddIntArrayToPool({:linear_in} one_loc_iv: One Loc, {:linear_in} intvec: IntArray) +modifies IntArrayPoolLow; +{ + call Map_Put(IntArrayPoolLow, one_loc_iv, intvec); +} +yield procedure {:layer 0} AddIntArrayToPool({:linear_in} one_loc_iv: One Loc, {:linear_in} intvec: IntArray); +refines Atomic_AddIntArrayToPool; + +//////////////////////////////////////////////////////////////////////////////// +// Low-level primitives for shared mutexes +type Tid; +type Mutex = Option Tid; +var {:layer 0, 9} MutexPool: Map Loc Mutex; + +right action {:layer 1, 9} Atomic_Mutex_Alloc() returns ({:linear} one_loc_l: One Loc) +modifies MutexPool; +{ + call one_loc_l := Loc_New(); + assume !Map_Contains(MutexPool, one_loc_l->val); + MutexPool := Map_Update(MutexPool, one_loc_l->val, None()); +} +yield procedure {:layer 0} Mutex_Alloc() returns ({:linear} one_loc_l: One Loc); +refines Atomic_Mutex_Alloc; + +right action {:layer 1, 9} Atomic_Mutex_Acquire({:linear} tid: One Tid, loc_l: Loc) +modifies MutexPool; +{ + assert Map_Contains(MutexPool, loc_l); + assume Map_At(MutexPool, loc_l) == None(); + MutexPool := Map_Update(MutexPool, loc_l, Some(tid->val)); +} +yield procedure {:layer 0} Mutex_Acquire({:linear} tid: One Tid, loc_l: Loc); +refines Atomic_Mutex_Acquire; + +left action {:layer 1, 9} Atomic_Mutex_Release({:linear} tid: One Tid, loc_l: Loc) +modifies MutexPool; +{ + assert Map_Contains(MutexPool, loc_l); + assert Map_At(MutexPool, loc_l) == Some(tid->val); + MutexPool := Map_Update(MutexPool, loc_l, None()); +} +yield procedure {:layer 0} Mutex_Release({:linear} tid: One Tid, loc_l: Loc); +refines Atomic_Mutex_Release; diff --git a/Test/civl/large-samples/shared-vector.bpl.expect b/Test/civl/large-samples/shared-vector.bpl.expect new file mode 100644 index 000000000..9b5e49582 --- /dev/null +++ b/Test/civl/large-samples/shared-vector.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 69 verified, 0 errors diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/large-samples/treiber-stack.bpl similarity index 100% rename from Test/civl/samples/treiber-stack.bpl rename to Test/civl/large-samples/treiber-stack.bpl diff --git a/Test/civl/samples/treiber-stack.bpl.expect b/Test/civl/large-samples/treiber-stack.bpl.expect similarity index 100% rename from Test/civl/samples/treiber-stack.bpl.expect rename to Test/civl/large-samples/treiber-stack.bpl.expect