kovan_map/hashmap/resize.rs
1//! Replacing the table: a resize copies it into a table of another capacity, a clear replaces it
2//! by an empty one. Both take the single resizer latch, freeze every link of the old table in
3//! chain order (copying, for a resize, each node that is not deleted), and publish the new table
4//! with the exact count of what it holds.
5//!
6//! Freezing is what makes a write final: every write is one CAS on one link, and a frozen link
7//! fails every CAS a writer makes (it expects the word without the flag). A write whose CAS
8//! landed before the freeze reached its link is in the chain the copy reads; a write that meets
9//! a frozen link waits for the new table and writes there. No write lands in a table after its
10//! copy read the link, so no landed write is lost and none is retried: an insert that landed
11//! never meets its own copy and never reports it as another caller's entry, and a remove never
12//! removes a copy of what it already removed. Modelled in `proofs/tla/chained/ChainedMap.tla`
13//! (actions Z0 to Z6), where 0.1.20's read-then-revalidate protocol (Mutation "revalidate")
14//! breaks both.
15
16use super::node::{FROZEN, Node, is_frozen, is_held, is_marked, ptr, with, word};
17use super::table::TableRef;
18use super::{HashMap, MIN_CAPACITY};
19use crate::MaybeSend;
20use crate::sync::spin_hint;
21use core::hash::{BuildHasher, Hash};
22use core::sync::atomic::Ordering;
23use kovan::{Atomic, Guard, Shared, alloc_node, pin, retire_node};
24
25extern crate alloc;
26
27impl<K, V, S> HashMap<K, V, S>
28where
29 K: Hash + Eq + Clone + MaybeSend + 'static,
30 V: Clone + MaybeSend + 'static,
31 S: BuildHasher,
32{
33 /// Spin until the resize or clear in flight has published its table (a writer that met a
34 /// frozen link, its guard dropped).
35 #[inline]
36 pub(super) fn wait_for_resize(&self) {
37 while self.resizing.load(Ordering::Acquire) {
38 spin_hint();
39 }
40 }
41
42 /// Resize the table to `new_capacity` buckets (the single resizer wins; a call that finds
43 /// the latch taken returns at once).
44 pub(super) fn try_resize(&self, new_capacity: usize) {
45 if self
46 .resizing
47 .compare_exchange(false, true, Ordering::Acquire, Ordering::Relaxed)
48 .is_err()
49 {
50 return;
51 }
52 let new_capacity = new_capacity
53 .next_power_of_two()
54 .max(MIN_CAPACITY)
55 .max(self.floor);
56 let guard = pin();
57 let old = self.table_ref(&guard);
58 if old.capacity() != new_capacity {
59 let new = TableRef::alloc(new_capacity);
60 // A `K::clone` or `V::clone` that panics in the migration unwinds through this,
61 // which undoes it (see `Undo`): the old table stays current and every writer goes
62 // on, where the latch held for good would have stopped them all.
63 let undo = Undo {
64 old,
65 new,
66 guard: &guard,
67 latch: &self.resizing,
68 };
69 let copied = Self::migrate(old, Some(new), &guard);
70 core::mem::forget(undo);
71 // Relaxed: the table's publication below releases it.
72 new.count().store(copied as isize, Ordering::Relaxed);
73 self.publish(old, new);
74 }
75 drop(guard);
76 self.resizing.store(false, Ordering::Release);
77 }
78
79 /// Clears the map, removing all key-value pairs.
80 ///
81 /// Linearizes when the empty table is published: a write that landed before its link was
82 /// frozen is cleared, a write that met a frozen link lands in the empty table after.
83 pub fn clear(&self) {
84 while self
85 .resizing
86 .compare_exchange(false, true, Ordering::Acquire, Ordering::Relaxed)
87 .is_err()
88 {
89 spin_hint();
90 }
91 let guard = pin();
92 let old = self.table_ref(&guard);
93 Self::migrate(old, None, &guard);
94 self.publish(old, TableRef::alloc(old.capacity()));
95 drop(guard);
96 self.resizing.store(false, Ordering::Release);
97 }
98
99 /// Freeze `link` and return its frozen word. A held link is waited for: only its holder
100 /// writes it, and the conditional write holding it lands in this table before the link
101 /// freezes (so the copy reads it).
102 fn freeze(link: &Atomic<Node<K, V>>, guard: &Guard) -> *mut Node<K, V> {
103 loop {
104 // A word a failed CAS returns is reloaded here rather than used: only a load
105 // protects the node it names.
106 let w = link.load(Ordering::Acquire, guard).as_raw();
107 if is_frozen(w) {
108 return w;
109 }
110 if is_held(w) {
111 spin_hint();
112 continue;
113 }
114 let frozen = with(w, FROZEN);
115 // AcqRel: the copy below reads the fields of the node the word names.
116 if link
117 .compare_exchange(
118 word(w),
119 word(frozen),
120 Ordering::AcqRel,
121 Ordering::Relaxed,
122 guard,
123 )
124 .is_ok()
125 {
126 return frozen;
127 }
128 }
129 }
130
131 /// Freeze every link of `old`, bucket by bucket in chain order, and copy each node that is
132 /// not deleted into `into` (a table no other thread sees yet). Returns the number copied.
133 fn migrate(old: TableRef<K, V>, into: Option<TableRef<K, V>>, guard: &Guard) -> usize {
134 let mut copied = 0;
135 for b in 0..old.capacity() {
136 let mut w = Self::freeze(old.bucket(b), guard);
137 loop {
138 let cur = ptr(w);
139 if cur.is_null() {
140 break;
141 }
142 // SAFETY: the frozen link that names it named it when this thread froze it, and
143 // a frozen link never changes, so it stays reachable (never retired) from here.
144 let node = unsafe { &*cur };
145 w = Self::freeze(&node.next, guard);
146 if is_marked(w) {
147 continue;
148 }
149 if let Some(new) = into {
150 let dst = new.bucket(new.bucket_index(node.hash));
151 let copy = Node::new(node.hash, node.key.clone(), node.value.clone());
152 // Relaxed: `new` is private to this thread until its publication releases it.
153 copy.next
154 .store(dst.load(Ordering::Relaxed, guard), Ordering::Relaxed);
155 dst.store(word(alloc_node(copy)), Ordering::Relaxed);
156 copied += 1;
157 }
158 }
159 }
160 copied
161 }
162
163 /// Make `new` the current table and retire `old`, every link of which is frozen.
164 fn publish(&self, old: TableRef<K, V>, new: TableRef<K, V>) {
165 // Release: a thread that acquires the new table sees its buckets, nodes and count.
166 // SAFETY: `new` is a live table allocation.
167 self.table
168 .store(unsafe { Shared::from_raw(new.as_raw()) }, Ordering::Release);
169 // SAFETY: the old table is unreachable from the map now; kovan frees it (and the nodes
170 // its frozen chains hold) once no guard that loaded it remains. TableProxy is
171 // #[repr(C)] with its RetiredNode at offset 0.
172 unsafe { retire_node(old.take_proxy()) };
173 }
174}
175
176/// Undoes a migration that unwinds (a clone of a key or value panicked in it): the links it
177/// froze in the old table thawed, the new table (no other thread ever saw it) freed with the
178/// copies made so far, and the latch let go, so the map goes on with its old table.
179struct Undo<'a, K: 'static, V: 'static> {
180 old: TableRef<K, V>,
181 new: TableRef<K, V>,
182 guard: &'a Guard,
183 latch: &'a crate::sync::AtomicBool,
184}
185
186impl<K: 'static, V: 'static> Drop for Undo<'_, K, V> {
187 fn drop(&mut self) {
188 thaw_links(self.old, self.guard);
189 // SAFETY: never published, so this thread alone reaches it and its copies.
190 unsafe { self.new.free() };
191 self.latch.store(false, Ordering::Release);
192 }
193}
194
195/// Clears the frozen flag of every link a migration froze in `table`: what a migration that
196/// cannot finish leaves behind. A migration freezes each chain from its head in order, so
197/// the frozen links of a chain are a prefix of it; while the latch is held no other thread
198/// changes a frozen link (a writer that meets one waits for the latch).
199fn thaw_links<K: 'static, V: 'static>(table: TableRef<K, V>, guard: &Guard) {
200 for b in 0..table.capacity() {
201 let mut link = table.bucket(b);
202 loop {
203 let w = link.load(Ordering::Acquire, guard).as_raw();
204 if !is_frozen(w) {
205 break;
206 }
207 let thawed = w.map_addr(|a| a & !FROZEN);
208 // AcqRel: a writer that loads the thawed word sees the chain as it was.
209 let _ = link.compare_exchange(
210 word(w),
211 word(thawed),
212 Ordering::AcqRel,
213 Ordering::Relaxed,
214 guard,
215 );
216 let cur = ptr(w);
217 if cur.is_null() {
218 break;
219 }
220 // SAFETY: a frozen link that names it named it while this thread froze it, so it
221 // is reachable and never retired while the guard is held.
222 link = unsafe { &(*cur).next };
223 }
224 }
225}