Skip to content

Commit d3b3d3c

Browse files
authored
Merge pull request #11 from ReshiAdavan/Sentinel-11
Sentinel-11: linearizability comment thru
2 parents 6c00b1e + 828961f commit d3b3d3c

File tree

4 files changed

+133
-97
lines changed

4 files changed

+133
-97
lines changed

linearizability/bitset.go

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,49 +1,57 @@
11
package linearizability
22

3+
// bitset is a type representing a set of bits.
34
type bitset []uint64
45

5-
// data layout:
6-
// bits 0-63 are in data[0], the next are in data[1], etc.
7-
6+
// newBitset creates a new bitset with a specified number of bits.
87
func newBitset(bits uint) bitset {
98
extra := uint(0)
9+
// Determine if an extra chunk is needed for the remaining bits.
1010
if bits%64 != 0 {
1111
extra = 1
1212
}
13+
// Calculate total number of 64-bit chunks needed.
1314
chunks := bits/64 + extra
1415
return bitset(make([]uint64, chunks))
1516
}
1617

18+
// clone creates a copy of the bitset.
1719
func (b bitset) clone() bitset {
1820
dataCopy := make([]uint64, len(b))
1921
copy(dataCopy, b)
2022
return bitset(dataCopy)
2123
}
2224

25+
// bitsetIndex calculates the index of the 64-bit chunk and the bit position within that chunk.
2326
func bitsetIndex(pos uint) (uint, uint) {
2427
return pos / 64, pos % 64
2528
}
2629

30+
// set sets the bit at the specified position to 1.
2731
func (b bitset) set(pos uint) bitset {
2832
major, minor := bitsetIndex(pos)
2933
b[major] |= (1 << minor)
3034
return b
3135
}
3236

37+
// clear sets the bit at the specified position to 0.
3338
func (b bitset) clear(pos uint) bitset {
3439
major, minor := bitsetIndex(pos)
3540
b[major] &^= (1 << minor)
3641
return b
3742
}
3843

44+
// get returns true if the bit at the specified position is 1.
3945
func (b bitset) get(pos uint) bool {
4046
major, minor := bitsetIndex(pos)
4147
return b[major]&(1<<minor) != 0
4248
}
4349

50+
// popcnt returns the total number of bits set to 1 in the bitset.
4451
func (b bitset) popcnt() uint {
4552
total := uint(0)
4653
for _, v := range b {
54+
// Hamming weight algorithm to count set bits efficiently.
4755
v = (v & 0x5555555555555555) + ((v & 0xAAAAAAAAAAAAAAAA) >> 1)
4856
v = (v & 0x3333333333333333) + ((v & 0xCCCCCCCCCCCCCCCC) >> 2)
4957
v = (v & 0x0F0F0F0F0F0F0F0F) + ((v & 0xF0F0F0F0F0F0F0F0) >> 4)
@@ -53,6 +61,7 @@ func (b bitset) popcnt() uint {
5361
return total
5462
}
5563

64+
// hash computes a hash value for the bitset, useful in hash-based collections.
5665
func (b bitset) hash() uint64 {
5766
hash := uint64(b.popcnt())
5867
for _, v := range b {
@@ -61,6 +70,7 @@ func (b bitset) hash() uint64 {
6170
return hash
6271
}
6372

73+
// equals checks if two bitsets are equal.
6474
func (b bitset) equals(b2 bitset) bool {
6575
if len(b) != len(b2) {
6676
return false

linearizability/linearizability.go

Lines changed: 41 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -6,56 +6,53 @@ import (
66
"time"
77
)
88

9+
// Define the type for specifying the kind of entry in history.
910
type entryKind bool
1011

12+
// Constants for differentiating call and return entries.
1113
const (
1214
callEntry entryKind = false
1315
returnEntry = true
1416
)
1517

18+
// entry represents a single operation (call or return) in the history.
1619
type entry struct {
1720
kind entryKind
18-
value interface{}
19-
id uint
20-
time int64
21+
value interface{} // Value associated with the operation.
22+
id uint // Unique identifier for the operation.
23+
time int64 // Timestamp of the operation.
2124
}
2225

26+
// byTime implements sort.Interface for sorting entries by their timestamp.
2327
type byTime []entry
2428

25-
func (a byTime) Len() int {
26-
return len(a)
27-
}
28-
29-
func (a byTime) Swap(i, j int) {
30-
a[i], a[j] = a[j], a[i]
31-
}
32-
33-
func (a byTime) Less(i, j int) bool {
34-
return a[i].time < a[j].time
35-
}
29+
func (a byTime) Len() int { return len(a) }
30+
func (a byTime) Swap(i, j int) { a[i], a[j] = a[j], a[i] }
31+
func (a byTime) Less(i, j int) bool { return a[i].time < a[j].time }
3632

33+
// makeEntries converts a slice of Operations to a slice of entries, sorted by time.
3734
func makeEntries(history []Operation) []entry {
38-
var entries []entry = nil
35+
var entries []entry
3936
id := uint(0)
4037
for _, elem := range history {
41-
entries = append(entries, entry{
42-
callEntry, elem.Input, id, elem.Call})
43-
entries = append(entries, entry{
44-
returnEntry, elem.Output, id, elem.Return})
38+
entries = append(entries, entry{callEntry, elem.Input, id, elem.Call})
39+
entries = append(entries, entry{returnEntry, elem.Output, id, elem.Return})
4540
id++
4641
}
4742
sort.Sort(byTime(entries))
4843
return entries
4944
}
5045

46+
// node represents a node in a doubly linked list of entries.
5147
type node struct {
52-
value interface{}
53-
match *node // call if match is nil, otherwise return
54-
id uint
55-
next *node
56-
prev *node
48+
value interface{} // Value associated with the node.
49+
match *node // Corresponding call/return node. For call entries, match is nil.
50+
id uint // Unique identifier for the operation.
51+
next *node // Next node in the list.
52+
prev *node // Previous node in the list.
5753
}
5854

55+
// insertBefore inserts a new node before the 'mark' node in the list.
5956
func insertBefore(n *node, mark *node) *node {
6057
if mark != nil {
6158
beforeMark := mark.prev
@@ -69,6 +66,7 @@ func insertBefore(n *node, mark *node) *node {
6966
return n
7067
}
7168

69+
// length calculates the length of the linked list starting from 'n'.
7270
func length(n *node) uint {
7371
l := uint(0)
7472
for n != nil {
@@ -78,9 +76,10 @@ func length(n *node) uint {
7876
return l
7977
}
8078

79+
// renumber reassigns unique identifiers to events in the history.
8180
func renumber(events []Event) []Event {
8281
var e []Event
83-
m := make(map[uint]uint) // renumbering
82+
m := make(map[uint]uint) // Map for renumbering.
8483
id := uint(0)
8584
for _, v := range events {
8685
if r, ok := m[v.Id]; ok {
@@ -94,6 +93,7 @@ func renumber(events []Event) []Event {
9493
return e
9594
}
9695

96+
// convertEntries converts a slice of Events to a slice of entries.
9797
func convertEntries(events []Event) []entry {
9898
var entries []entry
9999
for _, elem := range events {
@@ -106,9 +106,10 @@ func convertEntries(events []Event) []entry {
106106
return entries
107107
}
108108

109+
// makeLinkedEntries creates a doubly linked list of entries from a slice of entries.
109110
func makeLinkedEntries(entries []entry) *node {
110111
var root *node = nil
111-
match := make(map[uint]*node)
112+
match := make(map[uint]*node) // Map to track corresponding call/return nodes.
112113
for i := len(entries) - 1; i >= 0; i-- {
113114
elem := entries[i]
114115
if elem.kind {
@@ -125,11 +126,13 @@ func makeLinkedEntries(entries []entry) *node {
125126
return root
126127
}
127128

129+
// cacheEntry is used for caching the states encountered during the linearization check.
128130
type cacheEntry struct {
129-
linearized bitset
130-
state interface{}
131+
linearized bitset // Bitset representing the linearized operations.
132+
state interface{} // State of the model after these operations.
131133
}
132134

135+
// cacheContains checks if a given cache entry is already in the cache.
133136
func cacheContains(model Model, cache map[uint64][]cacheEntry, entry cacheEntry) bool {
134137
for _, elem := range cache[entry.linearized.hash()] {
135138
if entry.linearized.equals(elem.linearized) && model.Equal(entry.state, elem.state) {
@@ -139,11 +142,13 @@ func cacheContains(model Model, cache map[uint64][]cacheEntry, entry cacheEntry)
139142
return false
140143
}
141144

145+
// callsEntry represents an entry in the list of ongoing calls.
142146
type callsEntry struct {
143147
entry *node
144-
state interface{}
148+
state interface{} // Model state after the call.
145149
}
146150

151+
// lift removes an entry and its match from the linked list.
147152
func lift(entry *node) {
148153
entry.prev.next = entry.next
149154
entry.next.prev = entry.prev
@@ -154,6 +159,7 @@ func lift(entry *node) {
154159
}
155160
}
156161

162+
// unlift re-inserts an entry and its match back into the linked list.
157163
func unlift(entry *node) {
158164
match := entry.match
159165
match.prev.next = match
@@ -164,6 +170,7 @@ func unlift(entry *node) {
164170
entry.next.prev = entry
165171
}
166172

173+
// checkSingle checks if a single partition of the history is linearizable.
167174
func checkSingle(model Model, subhistory *node, kill *int32) bool {
168175
n := length(subhistory) / 2
169176
linearized := newBitset(n)
@@ -213,6 +220,7 @@ func checkSingle(model Model, subhistory *node, kill *int32) bool {
213220
return true
214221
}
215222

223+
// fillDefault fills in default implementations for missing methods in the model.
216224
func fillDefault(model Model) Model {
217225
if model.Partition == nil {
218226
model.Partition = NoPartition
@@ -226,14 +234,12 @@ func fillDefault(model Model) Model {
226234
return model
227235
}
228236

237+
// CheckOperations checks if the operations in the history are linearizable.
229238
func CheckOperations(model Model, history []Operation) bool {
230239
return CheckOperationsTimeout(model, history, 0)
231240
}
232241

233-
/*
234-
* Timeout = 0 means no timeout if this operation times out, then a false positive is possible
235-
*/
236-
242+
// CheckOperationsTimeout checks if the operations in the history are linearizable with a timeout.
237243
func CheckOperationsTimeout(model Model, history []Operation, timeout time.Duration) bool {
238244
model = fillDefault(model)
239245
partitions := model.Partition(history)
@@ -271,14 +277,12 @@ loop:
271277
return ok
272278
}
273279

280+
// CheckEvents checks if the events in the history are linearizable.
274281
func CheckEvents(model Model, history []Event) bool {
275282
return CheckEventsTimeout(model, history, 0)
276283
}
277284

278-
/*
279-
* timeout = 0 means no timeout if this operation times out, then a false positive is possible
280-
*/
281-
285+
// CheckEventsTimeout checks if the events in the history are linearizable with a timeout.
282286
func CheckEventsTimeout(model Model, history []Event, timeout time.Duration) bool {
283287
model = fillDefault(model)
284288
partitions := model.PartitionEvent(history)

linearizability/model.go

Lines changed: 29 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,48 +1,61 @@
11
package linearizability
22

3+
// Operation represents an operation in the history of a linearizability check.
4+
// It includes both the input to and output from the operation along with their respective timestamps.
35
type Operation struct {
4-
Input interface{}
5-
Call int64 // invocation time
6-
Output interface{}
7-
Return int64 // response time
6+
Input interface{} // Input of the operation.
7+
Call int64 // Invocation time of the operation.
8+
Output interface{} // Output of the operation.
9+
Return int64 // Response time of the operation.
810
}
911

12+
// EventKind is a type to distinguish between call and return events.
1013
type EventKind bool
1114

15+
// Constants for differentiating call and return events.
1216
const (
13-
CallEvent EventKind = false
14-
ReturnEvent EventKind = true
17+
CallEvent EventKind = false // Represents a call event.
18+
ReturnEvent EventKind = true // Represents a return event.
1519
)
1620

21+
// Event represents either a call or a return event in the history.
1722
type Event struct {
18-
Kind EventKind
19-
Value interface{}
20-
Id uint
23+
Kind EventKind // Kind of the event (CallEvent or ReturnEvent).
24+
Value interface{} // Value associated with the event.
25+
Id uint // Unique identifier for the event.
2126
}
2227

28+
// Model defines the structure of the system being checked for linearizability.
29+
// It includes functions for partitioning the history, initializing the system state,
30+
// stepping through the operations, and comparing system states.
2331
type Model struct {
24-
// Partition functions, such that a history is linearizable if an only
25-
// if each partition is linearizable.
32+
// Partition functions divide the history into parts, each of which must be linearizable.
2633
Partition func(history []Operation) [][]Operation
2734
PartitionEvent func(history []Event) [][]Event
28-
// Initial state of the system.
35+
36+
// Init initializes the system's state.
2937
Init func() interface{}
30-
// Step function for the system. Returns whether or not the system
31-
// could take this step with the given inputs and outputs and also
32-
// returns the new state. This should not mutate the existing state.
38+
39+
// Step function takes a state and an operation's input and output,
40+
// and returns whether the operation is valid in the current state and the new state.
41+
// It should not mutate the existing state.
3342
Step func(state interface{}, input interface{}, output interface{}) (bool, interface{})
34-
// Equality on states.
43+
44+
// Equal function defines equality for states.
3545
Equal func(state1, state2 interface{}) bool
3646
}
3747

48+
// NoPartition is a default partitioning function that treats the entire history as a single partition.
3849
func NoPartition(history []Operation) [][]Operation {
3950
return [][]Operation{history}
4051
}
4152

53+
// NoPartitionEvent is a default partitioning function for event histories, treating the entire history as a single partition.
4254
func NoPartitionEvent(history []Event) [][]Event {
4355
return [][]Event{history}
4456
}
4557

58+
// ShallowEqual is a default equality function that checks for basic equality between two states.
4659
func ShallowEqual(state1, state2 interface{}) bool {
4760
return state1 == state2
4861
}

0 commit comments

Comments
 (0)