1: % Modification of version of 28 July 2004

2: % Started 19 October 2004

3: \documentclass{article}

4: \usepackage[english]{babel}

5: %\usepackage{moreverb}

6: 

7: \usepackage{latexsym}

8: \usepackage{amssymb}

9: 

10: \newenvironment{tab}{\begin{tabbing}

11: MMMMM\=aaa\=aaa\=aaa\=aaa\=aaa\=aaa\= \kill}{\end{tabbing}}

12: 

13: \makeatletter

14: \def\refmystepcounter#1{\stepcounter{#1}\protect\gdef 

15: \@currentlabel {\csname p@#1\endcsname \csname 

16: the#1\endcsname}}

17: \makeatother

18: \newcounter {tabnr}

19: \newenvironment{tabn}{\begin{tabbing}

20: \refmystepcounter{tabnr}

21: MMMMM\=aaa\=aaa\=aaa\=aaa\=aaa\=aaa\= \kill

22: (\arabic{tabnr})~}{\end{tabbing}}

23: 

24: \newcommand{\nrule}{\refmystepcounter{tabnr}

25: \mbreak(\arabic{tabnr})~}

26: 

27: \newenvironment{ta}{\begin{tabbing}

28: MM\=aa\=aa\=aa\=aa\=aa\=aa\= \kill}{\end{tabbing}}

29: 

30: \def\boks  {\mbox{$\Box$}}

31: \def\Nat   {\mbox{$\mathbb{N}$}}

32: \def\IB    {\mbox{$\mathbb{B}$}}

33: \def\IR    {\mbox{$\mathbb{R}$}}

34: \def\IC    {\mbox{$\mathbb{C}$}}

35: \def\IP    {\mbox{$\mathbb{P}$}}

36: \def\IQ    {\mbox{$\mathbb{Q}$}}

37: \def\IZ    {\mbox{$\mathbb{Z}$}}

38: \def\Oh{{\cal O}}

39: \def\OPEN  {\mbox{$|\![ \: $}}

40: \def\CLOSE {\mbox{$\: ]\!| $}}

41: \def\bar   {\mbox{$[ \! ]$}}

42: \def\ang   {\mbox{$\,\diamondsuit\,$}}

43: \def\all   {\forall\;}

44: \def\ex    {\exists\;}

45: \def\sqleq {\sqsubseteq}

46: \def\omit#1{}

47: \def\S #1/{\mbox {\textsl{#1}}}

48: \def\B #1/{\mbox {\textbf{#1}}}

49: \def\R #1/{\mbox {\textrm{#1}}}

50: \def\T #1/{\mbox {\texttt{#1}}}

51: \def\from {\:\leftarrow\:}

52: \def\leadsto    {\mbox{$\:o\!\!\to\:$}}

53: \def\Leadsto    {\mbox{$\quad o\!\!\to\quad $}}

54: \def\la    {\mbox{$\langle$}}

55: \def\ra    {\mbox{$\rangle$}}

56: \def\Com   {\mbox {$\quad\{ $}}

57: \def\com   {\mbox {$ \{ $}}

58: \def\moc   {\mbox {$ \}\; $}}

59: \def\Moc   {\mbox {$ \}\quad $}}

60: \def\comm  {\mbox {$ (*\; $}}

61: \def\Comm  {\mbox {\quad $ (*\; $}}

62: \def\mmoc  {\mbox {$ \;*) $}}

63: \def\eps   {{\mbox{$\varepsilon$}}}

64: \def\phi   {{\mbox{$\varphi$}}}

65: \def\implies{\mbox{$\Rightarrow $}}

66: \def\follows{\mbox{$\Leftarrow $}}

67: \def\Implies{\mbox{$\;\Rightarrow\; $}}

68: \def\IMPLIES{\mbox{$\quad\Rightarrow\quad $}}

69: \def\EQ     {\mbox{\quad$\equiv$\quad}}

70: \def\eq     {\mbox{$\equiv\,$}}

71: \def\LAND   {\mbox{\quad$\land$\quad}}

72: \def\Land   {\mbox{ $\;\land\;$ }}

73: \def\LOR    {\mbox{$\quad\lor\quad$}}

74: \def\Lor    {\mbox{$\;\lor\;$}}

75: \def\LEQ    {\mbox{$\quad\leq\quad$}}

76: \def\TO     {\mbox{$\quad\to\quad$}}

77: \def\true   {\S true/}

78: \def\false  {\S false/}

79: \def\IS     {\mbox{$\quad =\quad $}}

80: \def\remark {\medbreak\noindent{\sl Remark.\/} }

81: \def\remarks{\medbreak\noindent{\sl Remarks.\/} }

82: \def\sbreak {\smallbreak\noindent}

83: \def\mbreak {\medbreak\noindent}

84: \def\bbreak {\bigbreak\noindent}

85: \def\proof  {\mbreak{\sl Proof.\/} }

86: \def\example{\mbreak{\sl Example.\/} }

87: \def\MIN    {\T MIN /}

88: \def\MAX    {\T MAX /}

89: \def\min    {\B\ min /}

90: \def\max    {\B\ max /}

91: \def\DOTS   {\mbox{\ .\ .\ }}

92: \def\half   {\mbox{$1\over 2$}}

93: \def\bol    {\mbox{$\bullet$}}

94: 

95: \newcounter{theoremcnt}[section]

96: \newcommand{\qed}{\hfill$\quad\Box$}

97: \renewcommand{\thetheoremcnt}{\thesection.\arabic{theoremcnt}}

98: 

99: \newenvironment{Tm}%

100: {\begin{trivlist}\refstepcounter{theoremcnt}

101: \item[]\bf Theorem~\thetheoremcnt.~\rm}{\end{trivlist}}

102: 

103: \pagestyle {myheadings}

104: \markright{\hfill Lock-free Dynamic Hash Tables --  }

105: 

106: \begin{document}

107: 

108: \begin {center}

109: {\Large\bf Lock-free Dynamic Hash Tables \\

110: with Open Addressing}\\

111: \mbox{}\\

112: Gao, H.$^1$, Groote, J.F.$^2$, Hesselink, W.H.$^1$\\

113: {\small

114: $^1$ Department of Mathematics and Computing Science, University of 

115: Groningen,\\

116: P.O. Box 800, 9700 AV  Groningen, The Netherlands (Email: 

117: \verb!{hui,wim}@cs.rug.nl!)\\

118: $^2$ Department of Mathematics and Computing Science, 

119: Eindhoven University of Technology, P.O. Box 513, 5600 MB  

120: Eindhoven, The Netherlands and CWI,\\ 

121: P.O. Box 94079, 1090 GB  Amsterdam, The Netherlands 

122: (Email: \verb!jfg@win.tue.nl!)}

123: \end{center}

124: 

125: \begin{abstract}

126: 

127: \noindent 

128: We present an efficient lock-free algorithm for parallel 

129: accessible hash tables with open addressing, which promises more 

130: robust performance and reliability than conventional lock-based 

131: implementations. ``Lock-free'' means that it is guaranteed 

132: that always at least one process completes its operation within 

133: a bounded number of steps. For a single processor architecture 

134: our solution is as efficient as sequential hash tables. On a 

135: multiprocessor architecture this is also the case when all 

136: processors have comparable speeds. The algorithm allows processors 

137: that have widely different speeds or come to a halt. It can easily be 

138: implemented using C-like languages and requires on average only 

139: constant time for insertion, deletion or accessing of elements. 

140: The algorithm allows the hash tables to grow and shrink when needed. 

141: 

142: Lock-free algorithms are hard to 

143: design correctly, even when apparently straightforward. Ensuring 

144: the correctness of the design at the earliest possible stage is a 

145: major challenge in any responsible system development. In view of 

146: the complexity of the algorithm, we turned to the interactive 

147: theorem prover PVS for mechanical support. We employ standard 

148: deductive verification techniques to prove around 200 invariance 

149: properties of our algorithm, and describe how this is achieved with

150: the theorem prover PVS.

151: \end{abstract}

152: 

153: \mbreak

154: {\it CR Subject Classification (1991):} 

155: {\sf D.1 Programming techniques}\\

156: {\it AMS Subject Classification (1991):} {\sf 68Q22 Distributed

157: algorithms, 68P20 Information storage and retrieval}\\

158: {\it Keywords \& Phrases:} {\sf Hash tables, Distributed algorithms, 

159: Lock-free, Wait-free}

160: 

161: \section{Introduction}

162: We are interested in efficient, reliable, parallel algorithms. 

163: The classical synchronization paradigm based on mutual exclusion

164: is not most suited for this, since mutual exclusion often turns 

165: out to be a performance bottleneck, and failure of a single process 

166: can force all other processes to come to a halt. This is the reason 

167: to investigate lock-free or wait-free concurrent objects, see e.g.\ 

168: \cite{Bar93,Her91,Her93,HeM92,HG99,KS97,LaMa94,Mic02,RaG02,ShS03,

169: SuT04,Valois94}. 

170: 

171: \subsubsection*{Lock-free and wait-free objects}

172: 

173: A \emph{concurrent object} is an abstract data type that 

174: permits concurrent operations that appear to be atomic

175: \cite{Her91,Lyn96,Valois94}.  The easiest way to implement 

176: concurrent objects is by means of mutual exclusion, but 

177: this leads to blocking when the process that holds 

178: exclusive access to the object is delayed or stops 

179: functioning.

180: 

181: The object is said to be \emph{lock-free} if any process 

182: can be delayed at any point without forcing any other 

183: process to block and when, moreover, it is guaranteed that 

184: always some process will complete its operation in a 

185: finite number of steps, regardless of the execution speeds 

186: of the processes \cite{Bar93,Her93,LaMa94,RaG02,Valois94}.

187: The object is said to be \emph{wait-free} when it is 

188: guaranteed that any process can complete any operation in 

189: a finite number of steps, regardless of the speeds of the 

190: other processes \cite {Her91}. 

191: 

192: We regard ``non-blocking'' as synonymous to ``lock-free''.  In several

193: recent papers, e.g. \cite{SuT04}, the term ``non-blocking'' is used

194: for the first conjunct in the above definition of lock-free. Note that

195: this weaker concept does not in itself guarantee progress. Indeed,

196: without real blocking, processes might delay each other arbitrarily

197: without getting closer to completion of their respective operations.

198: The older literature \cite{ARJ97,Bar93,HeM92} seems to suggest that

199: originally ``non-blocking'' was used for the stronger concept, and

200: lock-free for the weaker one. Be this as it may, we use lock-free 

201: for the stronger concept.

202: 

203: \subsubsection*{Concurrent hash tables}

204: 

205: The data type of hash tables is very commonly used to efficiently 

206: store huge but sparsely filled tables. Before 2003, as far as we 

207: know, no lock-free algorithm for hash tables had been 

208: proposed. There were general algorithms for arbitrary wait-free 

209: objects \cite{ABD90,BD89,Bar93,Her91,H95,H96}, but these are not 

210: very efficient. Furthermore, there are lock-free algorithms for 

211: different domains, such as linked lists \cite{Valois94}, queues 

212: \cite{Valois92} and memory management \cite{HeM92,HG99}.

213: 

214: In this paper we present a lock-free algorithm for hash 

215: tables with open addressing that is in several 

216: aspects wait-free.  The central idea is that every process 

217: holds a pointer to a hash table, which is the current one if the 

218: process is not delayed. When the current hash table is full, a new

219: hash table is allocated and all active processes join in the 

220: activity to transfer the contents of the current table to the new 

221: one. The consensus problem of the choice of a new table is solved 

222: by means of a test-and-set register. When all processes have left 

223: the obsolete table, it is deallocated by the last one leaving. This

224: is done by means of a compare-and-swap register. Measures have been 

225: taken to guarantee that actions of delayed processes are never 

226: harmful. For this purpose we use counters that can be incremented 

227: and decremented atomically. 

228: 

229: After the initial design, it took us several years to establish the 

230: safety properties of the algorithm. We did this by means of the 

231: proof assistant PVS \cite{OSR01}. Upon completion of this proof, we 

232: learned that a lock-free resizable hash table based on chaining was 

233: proposed in \cite{ShS03}. We come back to this below.

234: 

235: Our algorithm is lock-free and some of the subtasks are wait-free. 

236: We allow fully parallel \S insertion/, \S assignment/, \S deletion/, 

237: and \S finding/ of elements. Finding is wait-free, the other three 

238: are not. The primary cause is that the process executing it may 

239: repeatedly have to execute or join a migration of the hash table. 

240: Assignment and deletion are also not wait-free when other processes 

241: repeatedly assign to the same address successfully.

242: 

243: Migration is called for when the 

244: current hash table is almost filled. This occurs when the table has 

245: to grow beyond its current upper bound, but also for maintenance 

246: after many insertions and deletions. The migration itself is 

247: wait-free, but, in principle, it is possible that a slow process is 

248: unable to access and use a current hash table since the current hash 

249: table is repeatedly replaced by faster processes.

250: 

251: Migration requires subtle provisions, which can be best understood 

252: by considering the following scenario. Suppose that process $A$ is 

253: about to (slowly) insert an element in a hash table $H_1$. Before 

254: this happens, however, a fast process $B$ has performed migration

255: by making a new hash table $H_2$, and copying the content from 

256: $H_1$ to $H_2$. If (and only if) process $B$ did not copy the 

257: insertion of $A$, $A$ must be informed to move to the new hash table,

258: and carry out the insertion there. Suppose a process $C$ comes into

259: play also copying the content from $H_1$ to $H_2$. This must be

260: possible, since otherwise $B$ can stop copying, blocking all 

261: operations of other processes on the hash table, and thus violating 

262: the lock-free nature of the algorithm. Now the value inserted by 

263: $A$ can but need not be copied by both $B$ and/or $C$. This can be 

264: made more complex by a process $D$ that attempts to replace $H_2$ by 

265: $H_3$. Still, the value inserted by $A$ should show up exactly once 

266: in the hash table, and it is clear that processes should carefully 

267: keep each other informed about their activities on the tables.

268: 

269: \subsubsection*{Performance, comparison, and correctness}

270: 

271: For a single processor architecture our solution is of the same order

272: of efficiency as sequential hash tables. Actually, only an extra check

273: is required in the main loop of the main functions, one extra bit

274: needs to be set when writing data in the hashtables and at some places

275: a write operation has been replaced by a compare and swap, which is

276: more expensive.  For ordinary operations on the hashtable, this is the

277: only overhead and therefore a linear speed up can be expected on

278: multiprocessor systems. The only place where no linear speed up can be

279: achieved is when copying the hashtable. Especially, when processes

280: have widely different speeds, a logaritmic factor may come into play

281: (see algorithms for the write all problem \cite{Jan00,KS97}). Indeed,

282: initial experiments indicate that our algorithm is as efficient as

283: sequential hash tables. It seems to require on average only constant

284: time for insertion, deletion or accessing of elements.

285: 

286: Some differences between our algorithm and the algorithm of 

287: \cite{ShS03} are clear. In our algorithm, the hashed values need not 

288: be stored in dynamic nodes if the address-value pairs (plus one 

289: additional bit) fit into one word. 

290: Our hash table can shrink whereas the table of bucket headers in 

291: \cite{ShS03} cannot shrink. A disadvantage of our algorithm, due 

292: to its open addressing, is that migration is needed as maintenance 

293: after many insertions and deletions. 

294: 

295: An apparent weakness of our algorithm is the worst-case space

296: complexity in the order of $\Oh(P M)$ where $P$ is the number of

297: processes and $M$ is the size of the table. This only occurs when many

298: of the processes fail or fall asleep while using the hash

299: table. Failure while using the hash table can be made less probable by

300: adequate use of procedure ``releaseAccess''.  This gives a trade-off

301: between space and time since it introduces the need of a corresponding

302: call of ``getAccess''.  When all processes make ordinary progress and

303: the hash table is not too small, the actual memory requirement in

304: $\Oh(M)$.

305: 

306: The migration activity requires worst-case $\Oh(M^2)$ time for each 

307: participating process. This only occurs when the migrating processes

308: tend to choose the same value to migrate and the number of collisions 

309: is $\Oh(M)$ due to a bad hash function. 

310: This is costly, but even this is in agreement with 

311: wait-freedom. The expected amount of work for migration for all 

312: processes together is $\Oh(M)$ when collisions are sparse,

313: as should be the case when migrating to a hash table that is 

314: sufficiently large.

315: 

316: A true problem of lock-free algorithms is that they are hard to 

317: design correctly, which even holds for apparently straightforward 

318: algorithms. Whereas human imagination generally suffices to deal 

319: with all possibilities of sequential processes or synchronized

320: parallel processes, this appears impossible (at least to us) 

321: for lock-free algorithms. The only technique that we see fit 

322: for any but the simplest lock-free algorithms is to prove the 

323: correctness of the algorithm very precisely, and to verify this 

324: using a proof checker or theorem prover. 

325: 

326: As a correctness notion, we take that the operations behave the same 

327: as for `ordinary' hash tables, under some arbitrary linearization

328: \cite{HeW90} of these operations. So, if a \S find/ is carried out 

329: strictly after an \S insert/, the inserted element is found. If 

330: \S insert/ and \S find/ are carried out at the same time, it may be 

331: that \S find/ takes place before \S insertion/, and it is not 

332: determined whether an  element will be returned.

333: 

334: Our algorithm contains 81 atomic statements. The structure of our 

335: algorithm and its correctness properties, as well as the complexity 

336: of reasoning about them, makes neither automatic nor manual 

337: verification feasible. We have therefore chosen the higher-order 

338: interactive theorem prover PVS \cite{FCB00,OSR01} for mechanical 

339: support. PVS has a convenient specification language and contains 

340: a proof checker which allows users to construct proofs 

341: interactively, to automatically execute trivial proofs, and to 

342: check these proofs mechanically.

343: 

344: \subsubsection*{Overview of the paper}

345: 

346: Section \ref{interface} contains the description of the hash table 

347: interface offered to the users. The algorithm is presented in 

348: Section \ref{algorithm}. Section \ref{safety} contains a description 

349: of the proof of the safety properties of the algorithm: functional 

350: correctness, atomicity, and absence of memory loss. This proof is 

351: based on a list of around 200 invariants, presented in Appendix A, 

352: while the relationships between the invariants are given by a 

353: dependency graph in Appendix B. 

354: Progress of the algorithm is proved informally in Section 

355: \ref{progress}.

356: Conclusions are drawn in Section \ref{conclusions}.

357: 

358: \section{The interface}\label{interface}

359: 

360: The aim is to construct a hash table that can be 

361: accessed simultaneously by different processes in such 

362: a way that no process can passively block another 

363: process' access to the table. 

364: 

365: A hash table is an implementation of (partial) functions between 

366: two domains, here called \S Address/ and $\S Value/$. The hash 

367: table thus implements a modifiable shared variable 

368: $\T X/: \S Address/\to\S Value/$. 

369: The domains \S Address/ and \S Value/ both contain special 

370: default elements $0\in\S Address/$ and $\B null/\in\S Value/$. 

371: An equality $\T X/(a )=\B null/$ means that no value is currently 

372: associated with the address $a$. 

373: In particular, since we never store a value for the address $0$, 

374: we impose the invariant

375: \begin {tab}

376: \> $ \T X/(0)=\B null/$ .

377: \end {tab}

378: We use open addressing to keep all elements within the table.

379: For the implementation of the hash table we require 

380: that from every value the address it corresponds to is derivable. 

381: We therefore assume that some function 

382: $\S ADR/: \S Value/\to\S Address/$ is given with the property that 

383: \begin{tab} %ADRjective

384: \S Ax1:/ \>$~~~v=\B null/~\equiv ~ \S ADR/(v)= 0 $

385: \end{tab}

386: Indeed, we need \B null/ as the value corresponding to the undefined 

387: addresses and use address 0 as the (only) address associated with 

388: the value \B null/. We thus require the hash table to satisfy the 

389: invariant

390: \begin {tab}

391: \> $ \T X/(a) \ne \B null/\IMPLIES

392: \S ADR/(\T X/(a))= a$ .

393: \end {tab}

394: Note that the existence of \S ADR/ is not a real restriction since 

395: one can choose to store the pair $(a,v)$ instead of $v$. When $a$ 

396: can be derived from $v$, it is preferable to store $v$, since that 

397: saves memory.

398: 

399: There are four principle operations: \S find/, 

400: \S delete/, \S insert/ and \S assign/. 

401: The first one is to \S find/ the 

402: value currently associated with a given address. This 

403: operation yields $\B null/$ if the address has no associated value. 

404: The second operation is to \S delete/ the 

405: value currently associated with a given address. It fails

406: if the address was empty, i.e.\ $\T X/(a)=\B null/$.

407: The third operation is to \S insert/ a new value for a given 

408: address, provided the address was empty. So, note that

409: at least one out of two consecutive $\S insert/$s for address $a$

410: must fail, except when there is a $\S delete/$ for address $a$ in

411: between them. The operation $\S assign/$ does the same

412: as \S insert/, except that it rewrites the value even if the

413: associated address is not empty. Moreover, \S assign/ never fails.

414: 

415: We assume that there is a bounded number of processes that 

416: may need to interact with the hash table. Each process is 

417: characterized by the sequence of operations

418: \begin{tab}

419: \> $(\; \S getAccess/\;;\;

420:  (\S find/+\S delete/+\S insert/+\S assign/)^*\;;\;

421: \S releaseAccess/ )^\omega $ 

422: \end{tab}

423: A process that needs to access the table, first calls the 

424: procedure \S getAccess/ to get the current hash table pointer.

425: It may then invoke the procedures \S find/, \S delete/, \S insert/, 

426: and \S assign/ repeatedly, in an arbitrary, serial manner.

427: A process that has access to the table can call \S releaseAccess/ 

428: to log out. The processes may call these procedures concurrently. 

429: The only restriction is that every process can do at most one 

430: invocation at a time. 

431: 

432: The basic correctness conditions for concurrent systems are 

433: functional correctness and atomicity, say in the sense of 

434: \cite{Lyn96}, 

435: Chapter 13. Functional correctness is expressed by prescribing how 

436: the procedures \S find/, \S insert/, \S delete/, \S assign/ affect 

437: the value of the abstract mapping \T X/ in relation to the return 

438: value. Atomicity means that the effect on \T X/ and the return value

439: takes place atomically at some time between the invocation of the 

440: routine and its response. 

441: Each of these procedures has the precondition 

442: that the calling process has access to the table. In this 

443: specification, we use auxiliary private variables declared 

444: locally in the usual way. We give them the suffix $S$ to 

445: indicate that the routines below are the specifications of the 

446: procedures. We use angular brackets \la\ and \ra\ to indicate 

447: atomic execution of the enclosed command.

448: \begin {tab}

449: \> $ \B proc /\S find/_S (a:\S Address/\setminus\{0\}) : 

450: \S Value/ = $\\

451: \>\>\B local/ $rS:\S Value/$;\\

452: (fS) \>\>\la~$rS:=\; \T X/(a)\;\ra $;\\

453: \>\B return/ $rS$.

454: \end{tab}

455: 

456: \begin {tab}

457: \> $ \B proc /\S delete/_S (a:\S Address/\setminus\{0\}) : 

458: \S Bool/ = $\\

459: \>\>\B local/ $\S sucS/:\S Bool/$;\\

460: (dS) \>\>\la~$ \S sucS/:=(\T X/(a)\not=\B null/)$ ; \\

461: \>\>~~$ \B if /\;\S sucS/\; \B\ then /\;

462: \T X/(a):=\B null/\;\B\ end /\ra$ ;\\

463: \>\B return/ $\S sucS/$.

464: \end{tab}

465: 

466: \begin{tab}

467: \>\B proc/ $\S insert/_S (v:\S Value/\setminus\{\B null/\}) : 

468: \S Bool/ = $\\

469: \>\>\B local/ $\S sucS/:\S Bool/\;;\; a:\S Address/:= \S ADR/(v) $ ;\\

470: (iS) \>\>\la~$ \S sucS/:=(\T X/(a)=\B null/)$ ;\\

471: \>\>~~$ \B if /\;\S sucS/\; \B\ then /\; \T X/(a):=v\;\B\ end /\ra $ ;\\

472: \>\B return/ $\S sucS/$.

473: \end{tab}

474: 

475: \begin {tab}

476: \>$\B proc /\S assign/_S(v:\S Value/\setminus\{\B null/\})= $\\

477: \>\>\B local/ $ a:\S Address/:= \S ADR/(v) $ ;\\

478: (aS) \>\>\la~$\T X/(a):=v \; \ra $ ;\\

479: \>\B end/.

480: \end{tab}

481: Note that, in all cases, we require that the body of the 

482: procedure is executed atomically at some moment between the 

483: beginning and the end of the call, but that this moment need not 

484: coincide with the beginning or end of the call. This is the reason 

485: that we do not (e.g.) specify \S find/ by the single line 

486: $\B return /\T X/(a) $.

487: 

488: Due to the parallel nature of our system we cannot use pre and 

489: postconditions to specify it. For example, it may happen that 

490: $\S insert/(v)$ returns \true\ while $\T X/(\S ADR/(v))\ne v $ 

491: since another process deletes $\S ADR/(v)$ between the execution 

492: of (iS) and the response of \S insert/. 

493: 

494: In Section \ref{primary}, we provide implementations for the 

495: operations \S find/, \S delete/, \S insert/, \S assign/. 

496: We prove partial correctness of the implementations by extending them

497: with the auxiliary variables and commands used in the specification.

498: So, we regard \T X/ as a shared auxiliary variable and $rS$ 

499: and $\S sucS/$ as private auxiliary variables; we augment the 

500: implementations of \S find/, \S delete/, \S insert/, \S assign/ 

501: with the atomic commands (fS), (dS), (iS), (aS), respectively. 

502: We prove that each of the four implementations executes 

503: its specification command always exactly once and that the 

504: resulting value $r$ or $\S suc/$ of the implementation equals the 

505: resulting value $rS$ or $\S sucS/$ in the specification. It follows 

506: that, by removing the 

507: implementation variables from the combined program, we obtain the 

508: specification. This removal may eliminate many atomic steps of the 

509: implementation. This is known as removal of stutterings in TLA 

510: \cite{Lam94} or abstraction from $\tau$ steps in process algebras.

511: 

512: \section{The algorithm} \label{algorithm}

513: 

514: An implementation consists of $P$ processes along with a set of 

515: variables, for $P\geq 1$. Each process, numbered from $1$ up to $P$, 

516: is a sequential program comprised of atomic statements. Actions on 

517: private variables can be added to an atomic statement, but all 

518: actions on shared variables must be separated into atomic accesses.

519:  Since auxiliary variables are only used to facilitate the 

520: proof of correctness, they can be assumed to be touched instantaneously

521: without violation of the atomicity restriction. 

522: 

523: \subsection{Hashing}

524: 

525: We implement function \T X/ via hashing with open addressing, cf.\ 

526: \cite{Knuth3,Wir}. We do not use direct chaining, where colliding 

527: entries are stored in a secondary list, as is done in \cite {ShS03}.

528: A disadvantage of open addressing with deletion of elements is that 

529: the contents of the hash table must regularly be refreshed by copying 

530: the non-deleted elements to a new hash table. 

531: As we wanted to be able to resize the hash tables 

532: anyhow, we consider this less of a burden. 

533: 

534: In principle, hashing is a way to store address-value pairs 

535: in an array (hash table) with a length much smaller than the 

536: number of potential addresses. The indices of the array are 

537: determined by a hash function. In case the hash function maps 

538: two addresses to the same index in the array there 

539: must be some method to determine an alternative index. 

540: The question how to choose a good hash function and how to

541: find alternative locations in the case of open addressing is 

542: treated extensively elsewhere, e.g.\ \cite{Knuth3}.

543: 

544: For our purposes it is convenient to combine these two roles in 

545: one abstract function \S key/ given by:

546: \begin {tab}

547: \> $ \S key/(a: \S Address/,\;l:\S Nat/,\;n:\S Nat/):\S Nat/$ ,

548: \end {tab}

549: where $l$ is the length of the array (hash table), that satisfies 

550: \begin{tab}

551: \S Ax2:/ \>$ 0\leq \S key/(a,l,n) < l$ 

552: \end{tab}

553: for all $a$, $l$, and $n$. The number $n$ serves to 

554: obtain alternative locations in case of collisions: 

555: when there is a collision, we re-hash until an empty ``slot'' 

556: (i.e. \B null/) or the same address in the table is found.

557: The approach with a third argument $n$ is unusual but 

558: very general. It is more usual to have a function 

559: \S Key/ dependent on $a$ and $l$, and use a second 

560: function \S Inc/, which may depend on $a$ and $l$, to use in 

561: case of collisions. Then our function \S key/ is 

562: obtained recursively by 

563: \begin {tab}

564: \>\+ $ \S key/(a,l,0) = \S Key/(a,l)$ and 

565: $ \S key/(a,l,n+1) = \S Inc/(a,l,\S key/(a,l,n)) $ .

566: \end {tab}

567: We require that, for any address $a$ and any number $l$, 

568: the first $l$ keys are all different, as expressed in 

569: \begin {tab}

570: \S Ax3:/ \> $ 0\leq k < m < l \IMPLIES 

571: \S key/(a,l,k) \ne \S key/(a,l,m) $ .

572: \end {tab}

573: 

574: \subsection{Tagging of values}

575: 

576: As is well known \cite{Knuth3}, hashing with open addressing needs 

577: a special value $\B del/\in \S Value/$ to replace deleted values. 

578: 

579: When the current hash table becomes full, the processes need to reach 

580: consensus to allocate a new hash table of new size to replace the 

581: current one. Then all values except \B null/ and \B del/ must be 

582: migrated to the new hash table. A value that is being migrated 

583: cannot be simply removed, since the migrating process may stop 

584: functioning during the migration. Therefore, a value being copied 

585: must be tagged in such a way that it is still recognizable. This is 

586: done by the function \S old/. We thus introduce 

587: an extended domain of values to be called \S EValue/,

588: which is defined as follows:

589: \begin{tab}

590: \>\S EValue/ = $\{ \B del/\}\cup\S Value/\cup

591: \{\S old/(v)~|~v\in \S Value/\}$

592: \end{tab}

593: We furthermore assume the existence of functions

594: $\S val/: \S EValue/\to\S Value/$ and $\S oldp/: \S EValue/\to\S Bool/$ that satisfy, for all $v\in \S Value/$:

595: \begin{tab}

596: \>$\S val/(v)=v$ \>\>\>\>\>\> $\S oldp/(v)=\false$\\

597: \>$\S val/(\B del/)=\B null/$ \>\>\>\>\>\> $\S oldp/(\B del/)=\false$\\

598: \>$\S val/(\S old/(v))=v$ \>\>\>\>\>\> $\S oldp/(\S old/(v))=\true$ 

599: \end{tab}

600: Note that the \S old/ tag can easily be implemented by 

601: designating one special bit in the representation of \S Value/.

602: In the sequel we write $\B done/$ for $\S old/(\B null/)$.

603: Moreover, we extend the function $\S ADR/$ to domain $\S EValue/$

604: by $\S ADR/(v)=\S ADR/(\S val/(v))$.

605: 

606: \subsection {Data structure}

607: 

608: A \S Hash table/ is either $\bot$, indicating the absence of a 

609: hash table, or it has the following structure:

610: \begin{tab}

611: \>$\T size, bound, occ, dels/ :\S Nat/$;\\

612: \>$\T table/:\B array / 0\DOTS\T size-1 /\B of/ \S\ EValue/$.

613: \end{tab}

614: The field \T size/ indicates the size of the hash table, 

615: \T bound/ the maximal number of places that

616: can be occupied before refreshing the table. Both

617: are set when creating the table and remain constant. The 

618: variable \T occ/ gives the number of occupied positions in

619: the table, while the variable \T dels/ gives the number of deleted 

620: positions. If $h$ is a pointer to a hash table, we write 

621: $h.\T size/$, $h.\T occ/$, $h.\T dels/$ and 

622: $h.\T bound/$ to access these fields of the hash table. We write 

623: $h.\T table/[i]$ to access the $i^{\rm th}$ \S EValue/ in 

624: the table.

625: 

626: Apart from the \S current/ hash table, which is the main representative

627: of the variable \T X/, we have to deal with \S old/ hash tables, which 

628: were in use before the current one, and \S new/ hash tables, which can be

629:  created after the current one.

630:  

631: We now introduce data structures that are used by the processes

632: to find and operate on the hash table and allow to

633: delete hash tables that are not used anymore. The basic idea is

634: to count the number of processes that are using a hash table, 

635: by means of a counter \T busy/. The hash table can be thrown away when

636: \T busy/ is set to $0$. An important observation is that \T busy/ 

637: cannot be stored as part of the hash table, in the same way as 

638: the variables \T size/, \T occ/ and \T bound/ above. The reason 

639: for this is that a process can attempt to access the current 

640: hash table by increasing its \T busy/ counter. However, just 

641: before it wants to write the new value for \T busy/ it falls 

642: asleep. When the process wakes up the hash table might have been 

643: deleted and the process would be writing at a random place in 

644: memory.

645: 

646: This forces us to use separate arrays \T H/ and \T busy/ to store 

647: the pointers to hash tables and the \T busy/ counters. There

648: can be $2P$ hash tables around, because each process can

649: simultaneously be accessing one hash table and attempting to

650: create a second one. The arrays below are shared variables.

651: 

652: \begin {tab}

653: \>$\T H/:\B array /1\DOTS 2P \B\ of pointer to /\S Hashtable/$ ;\\

654: \>$\T busy/ :\B array /1\DOTS 2P \B\ of / \S Nat/$ ;\\

655: \>$\T prot/:\B array /1\DOTS 2P \B\ of / \S Nat/$ ;\\

656: \>$\T next/:\B\ array /1\DOTS 2P \B\ of /0\DOTS 2P$ .

657: \end {tab}

658: As indicated, we also need arrays \T prot/ and \T next/. The variable 

659: $\T next/[i]$ points to the next hash table to which the 

660: contents of hash table $\T H/[i]$ is being copied. 

661: If $\T next/[i]$ equals $0$, this means that there is no next 

662: hash table. The variable $\T prot/[i]$

663: is used to guard the variables $\T busy/[i]$, $\T next/[i]$ and

664: $\T H/[i]$ against being reused for a new table, before

665: all processes have discarded them.

666: 

667: We use a shared variable \T currInd/ to hold the index

668: of the currently valid hash table:

669: \begin {tab}

670: \>$\T currInd/:1\DOTS 2P$ .

671: \end {tab}

672: Note however that after a process copies $\T currInd/$ 

673: to its local memory, other processes may create a new 

674: hash table and change $\T currInd/$ to point to that one.

675: 

676: It is assumed that initially $\T H/[1]$ is pointing to 

677: some hash table. The other initial values of the shared 

678: variables are given by

679: \begin{tab}

680: \> $ \T currInd/ = \T busy/[1] = \T prot/[1] = 1 $ ,\\

681: \> $\T H/[i] = \T busy/[i] = 

682: \T prot/[i] = 0 $ \ for all $i\ne 1$ ,\\

683: \> $ \T next/[i] = 0 $ \ for all $i$.

684: \end{tab}

685: 

686: \subsection{Primary procedures} \label{primary}

687: 

688: We first provide the code for the primary procedures, which match

689: directly with the procedures in the interface. Every process has 

690: a private variable 

691: \begin{tab}

692: \>$\S index/:1\DOTS 2P$;

693: \end{tab}

694: containing what it regards as the currently active hash table.

695: At entry of each primary procedure, 

696: it must be the case that the variable $\T H/[\S index/]$

697: contains valid information. 

698: In section \ref{Mem}, we provide procedure \S getAccess/ with 

699: the main purpose to guarantee this property. 

700: When \S getAccess/ has been called, the system is obliged to 

701: keep the hash table at \S index/ stored in memory, even if there 

702: are no accesses to the hash table using any of the primary 

703: procedures. A procedure \S releaseAccess/ is provided to 

704: release resources, and it should be called whenever the 

705: process will not access the hash table for some time.

706: 

707: \subsubsection{Syntax}

708: 

709: We use a syntax analogous to Modula-3 \cite{Har92}. We use $:=$ for 

710: the assignment. We use the C--operations \T ++/ and 

711: \T --/ for atomic increments and decrements. 

712: The semicolon is a separator, not a terminator. 

713: The basic control mechanisms are

714: \begin{tab}

715: \> \B loop .. end / is an infinite loop, terminated by 

716: \B exit/ or \B return/\\

717: \> \B while .. do .. end / and \B repeat .. until .. / are 

718: ordinary loops\\

719: \> \B if .. then .. \{elsif ..\} [else ..] end / is the 

720: conditional\\

721: \> \B case .. end / is a case statement.

722: \end{tab}

723: Types are slanted and start with a capital. Shared variables 

724: and shared data elements are in typewriter font. Private variables 

725: are slanted or in math italic. 

726: 

727: \subsubsection{The main loop}

728: We model the clients of the hash table in the following loop. This 

729: is not an essential part of the algorithm, but it is needed in the

730: PVS description, and therefore provided here.

731: \begin {tab}

732: \>\B loop/\\

733: 0: \>\> $ \S getAccess/()$ ;\\

734: \>\>\B loop/\\

735: 1: \>\>\>$\S choose call; /\B case /call\ \B of /$\\

736: \>\>\>\> $(f,a)\ \B with /\ a\neq 0\rightarrow \S find/(a)$\\

737: \>\>\>\> $(d,a)\ \B with /\ a\neq 0\rightarrow \S delete/(a)$\\

738: \>\>\>\> $(i,v)\ \B with /\ v\neq \B null/\rightarrow 

739: \S insert/(v)$\\

740: \>\>\>\> $(a,v)\ \B with /\ v\neq \B null/\rightarrow 

741: \S assign/(v)$\\

742: \>\>\>\> $(r)\ \rightarrow \S releaseAccess/(\S index/);\ \B exit/$\\

743: \>\>\>\B end/\\

744: \>\>\B end/\\

745: \>\B end/

746: \end{tab}

747: The main loop shows that each process repeatedly invokes its four 

748: principle operations with correct arguments in an arbitrary, serial 

749: manner. Procedure \S getAccess/ has to provide the client with a 

750: protected value for \S index/. Procedure \S releaseAccess/ 

751: releases this value and its protection. Note that \B exit/ means 

752: a jump out of the inner loop.

753: 

754: \subsubsection{Procedure \S find/}

755: 

756: Finding an address in a hash table with open addressing requires 

757: a linear search over the possible hash keys until the address or 

758: an empty slot is found. The kernel of procedure \S find/ is 

759: therefore:

760: \begin {tab}

761: \>\+ $ n:= 0 $ ;\\

762: $ \B repeat /\; r:=h.\T table/[\S key/(a, l, n)] \;;\quad

763: n\T ++/ $ ;\\

764: $ \B until / \; r= \B null/\Lor a = \S ADR/(r) $ ;

765: \end{tab}

766: The main complication is that, when the process encounters an entry 

767: \B done/ (i.e. \S old/(\B null/)), it has to join the migration 

768: activity by calling \S refresh/. 

769: 

770: Apart from a number of special commands, we group statements

771: such that at most one shared variable is accessed and label these

772: `atomic' statements with a number. The labels are chosen identical 

773: to the labels in the PVS code, and therefore not completely 

774: consecutive.

775: 

776: In every execution step, one of the processes proceeds from 

777: one label to a next one. The steps are thus treated as 

778: atomic. The atomicity of steps that refer to shared variables 

779: more than once is emphasized by enclosing them in angular 

780: brackets. Since procedure calls only modify private control data, 

781: procedure headers are not always numbered themselves, but their bodies 

782: usually have numbered atomic statements.

783: %\newpage

784: \begin {tab}

785: \>$ \B proc /\S find/ (a:\S Address/\setminus\{0\}) : 

786: \S Value/= $\\

787: \>\>\B local/ $ r:\S EValue/$ ; $ n,l:\S Nat/\;;\; 

788: h:\B pointer to /\S Hashtable/$ ;\\

789: 5: \>\> $h:=\T H/[\S index/]\;;\; n:=0 \;;\;\{ \S cnt/:=0\}$ ;\\

790: 6: \>\> $l:=h.\T size/$ ;\\

791: \>\>\B repeat/\\

792: 7: \>\>\>\la~$r:=h.\T table/[\S key/(a, l, n)] $ ;\\

793: \>\>\>~~$\{ \B\ if /r= \B null/\Lor a=\S ADR/(r)\B\ then /\;

794: \S cnt/\T ++/\;;\;\R (fS)/ \;\B\ end /\}\;\ra $ ;\\

795: 8: \>\>\> \B if / $r=\B done/\;\B\ then /$\\

796: \>\>\>\> $ \S refresh/()$ ;\\

797: 10: \>\>\>\>$ h:=\T H/[\S index/]\;;\; n:=0$ ;\\

798: 11: \>\>\>\>$l:=h.\T size/$ ;\\

799: \>\>\>$ \B else /\; n\T ++/\; \B\ end/$ ;\\

800: 13: \>\>\B until/ $r= \B null/\Lor a=\S ADR/(r) $ ;\\

801: 14: \>\B return/ $\S val/(r)$ .

802: \end{tab}

803: 

804: In order to prove correctness, we add between braces 

805:  instructions that only modify auxiliary variables, like the 

806: specification variables \T X/ and $rS$ and other auxiliary 

807: variables to be introduced later.  

808: The part between braces is comment for the implementation, it 

809: only serves in the proof of correctness. The private auxiliary 

810: variable \S cnt/ of type \S Nat/ counts the number of times 

811: (fS) is executed and serves to prove that (fS) is executed 

812: precisely once in every call of \S find/. 

813: 

814: This procedure matches the code of an ordinary find in a hash table 

815: with open addressing, except for the code at the 

816: condition $r=\B done/$. This code is needed for the case that 

817: the value at address $a$ has been copied, in which case the new 

818: table must be located. Locating the new table is carried out 

819: by the procedure \S refresh/, which is discussed in Section 

820: \ref{Mem}. In line 7, the accessed hash table should be 

821: valid (see invariants \S fi4/ and \S He4/ in Appendix A).

822: After \S refresh/ the local variables $n$, $h$ and 

823: $l$ must be reset, to restart the search in the new hash table.

824: If the procedure terminates, the specifying atomic command (fS) 

825: has been executed precisely once (see invariant \S Cn1/) and the 

826: return values of the specification and the implementation are equal 

827: (see invariant \S Co1/). If the operation succeeds, 

828: the return value must be a valid entry currently associated with 

829: the given address in the current hash table. It is not evident but 

830: it has been proved that the linear search of the process executing 

831: \S find/ cannot be violated by other processes, i.e. no other 

832: process can \S delete/, \S insert/, or \S rewrite/ an entry 

833: associated with the same address (as what the process is looking 

834: for) in the region where the process has already searched. 

835: 

836: We require that every valid hash table contains at least one entry 

837: \B null/ or \B done/. Therefore, the local variable $n$ in the 

838: procedure \S find/ never goes beyond the size of the hash table 

839: (see invariants \S Cu1/, \S fi4/, \S fi5/ and axiom \S Ax2/).

840: When the \T bound/ of the new hash table is tuned properly before 

841: use (see invariants \S Ne7/, \S Ne8/), 

842: the hash table will not be updated too frequently, 

843: and termination of the procedure \S find/ can be guaranteed. 

844: 

845: \subsubsection{Procedure \S delete/}

846: 

847: To some extent, deletion is similar to finding. Since $r$ is a 

848: local variable to the procedure \S delete/, we regard 18a and 18b 

849: as two parts of atomic instruction 18. 

850:  If the entry is found in the table, then at line 18b this entry 

851: is overwritten with the designated element \B del/.

852: 

853: %\newpage

854: \begin {tab}

855: \> $ \B proc /\S delete/ (a:\S Address/\setminus\{0\}) : 

856: \S Bool/ = $\\

857: \>\>\B local/ $ r:\S EValue/\;;\; k,l,n:\S Nat/ $ ;\\

858: \>\>\> $ h:\B pointer to /\S Hashtable/\;;\;\S suc/:\S Bool/$ ;\\

859: 15: \>\> $h:=\T H/[\S index/]\;;\;\S suc/:=\; \false\;;\; 

860: \{\S cnt/:=0\} $ ;\\

861: 16: \>\>$l:=h.\T size/\;;\; n:=0$ ;\\

862: \>\>\B repeat/\\

863: 17: \>\>\> $k:=\S key/(a, l, n) $ ;\\

864: \>\>\> \la~$ r:=h.\T table/[k] $ ;\\

865: \>\>\>~~$\{\;\B  if /r=\B null/\;\B\ then /\;

866: \S cnt/\T ++/\;;\; \R (dS) /\B\ end /\}\;\ra $ ;\\

867: 18a: \>\>\> $ \B if /\;\S oldp/(r)\;\B\ then / $\\

868: \>\>\>\>  $ \S refresh/()$ ;\\

869: 20: \>\>\>\> $ h:=\T H/[\S index/]$ ; \\

870: 21: \>\>\>\> $ l:=h.\T size/\;;\; n:=0$ ;\\

871: \>\>\> $ \B elsif / \; a=\S ADR/(r)\;\B\ then / $\\

872: 18b:\>\>\>\> \la~$ \B if /\; r=h.\T table/[k] \;\B\ then /$\\

873: \>\>\>\>\>\>~~$\S suc/:= \true \;;\; h.\T table/[k] :=\B del/ $ ; \\

874: \>\>\>\>\>\>~~$\{\; \S cnt/\T ++/\;;\;\R (dS) /\;;\;

875: \T Y/[k] :=\B del/\ \}$\\

876: \>\>\>\>~~\B end /\ra\ ;\\

877: \>\>\> $\B else /\; n\T++/ \;\B\ end/ $ ; \\

878: \>\> $ \B until /\; \S suc/ \Lor r = \B null/ $ ;\\

879: 25: \>\> $ \B if /\; \S suc/\; \B\ then /\; 

880: h.\T dels/ \T ++/\;\B\ end/$ ;\\

881: 26: \> \B return/ \S suc/ .

882: \end{tab}

883: 

884: The repetition in this procedure has two ways to terminate.

885: Either deletion fails with $r=\B null/$ in 17, or deletion succeeds 

886: with $r=h.\T table/[k]$ in 18b. In the latter case, we have in one 

887: atomic statement a double access of the shared variable 

888: $h.\T table/[k]$. This is a so-called compare\&swap instruction. 

889: Atomicity is needed here to preclude interference. The specifying 

890: command (dS) is executed either in 17 or in 18b, and it is executed 

891: precisely once (see invariant \S Cn2/), since in 18b the guard 

892: $a=\S ADR/(r)$ implies $r\ne\B null/$ (see invariant 

893: \S de1/ and axiom \S Ax1/). 

894: 

895: In order to remember the address from the value rewritten 

896: to \B done/ after the value is 

897: being copied in the procedure \S moveContents/, in 18, we 

898: introduce a new auxiliary shared variable \T Y/ of type array 

899: of \S EValue/, whose contents 

900: equals the corresponding contents of the current hash table 

901: almost everywhere except that the values it contains are not 

902: tagged as \S old/ or rewritten as \B done/ (see invariants 

903: \S Cu9/, \S Cu10/).

904:  

905: Since we postpone the increment of \S h/.\T dels/ until line 25, 

906: the field \T dels/ is a lower bound of the number of positions 

907: deleted in the hash table (see invariant \S Cu4/). 

908: 

909: \subsubsection{Procedure \S insert/}

910: 

911: The procedure for insertion in the table is given below. 

912: Basically, it is the standard algorithm for insertion in a 

913: hash table with open addressing. Notable is line 28 where 

914: the current process finds that the current hash table too full, 

915: and orders a new table to be made.  

916: We assume that $h.\T bound/$ is a number less than 

917: $h.\T size/$ (see invariant \S Cu3/), which is tuned for optimal 

918: performance. 

919: 

920: Furthermore, in line 35, it can be detected that values in the 

921: hash table have been marked \S old/, which is a sign that 

922: hash table $h$ is outdated, and the new hash table must 

923: be located to perform the insertion.

924: \begin {tab}

925: \>$ \B proc /\S insert/ (v:\S Value/\setminus\{\B null/\}) : 

926: \S Bool/ = $\\

927: \>\> $ \B local / r:\S EValue/\;;\; k,l,n:\S Nat/\;;\;

928: h:\B pointer to /\S Hashtable/$ ;\\

929: \>\>\> $\S suc/:\S Bool/\;;\; a:\S Address/:= \S ADR/(v) $ ;\\

930: 27: \>\>$h:=\T H/[\S index/] \;;\; \{\S cnt/:=0\} $ ;\\

931: 28: \>\>\B if/ $h.\T occ/ > h.\T bound/\B\ then /$\\

932: \>\>\> $ \S newTable/()$ ;\\

933: 30: \>\>\> $h:=\T H/[\S index/]\; \B\ end/$ ;\\

934: 31: \>\> $ n:=0\;;\; l:=h.\T size/\;;\; \S suc/:= \false$ ;\\

935: \>\> \B repeat /\\

936: 32: \>\>\>$ k:=\; \S key/(a,l,n) $ ; \\

937: 33: \>\>\>\la~$ r:=h.\T table/[k] $ ; \\

938: \>\>\>~~$ \{\;\B if /\;a=\S ADR/(r)\;

939: \B\ then /\; \S cnt/\T ++/\;;\;\R\ (iS) /\B\ end /\}\;\ra $ ;\\

940: 35a: \>\>\>$ \B if /\;\S oldp/(r)\; \B\ then/ $ \\

941: \>\>\>\> $ \S refresh/()$ ;\\

942: 36: \>\>\>\> $h:=\T H/[\S index/]$ ;\\

943: 37: \>\>\>\> $n:=0\;;\; l:=h.\T size/$ ;\\

944: \>\>\> $ \B elsif / \; r = \B null/ \B\ then /$\\

945: 35b: \>\>\>\> \la~$ \B if /\; h.\T table/[k] = \B null/

946: \;\B\ then/$\\

947: \>\>\>\>\> $  \S suc/:=\true \;;\; h.\T table/[k] :=v $ ; \\

948: \>\>\>\>\> $ \{\; \S cnt/\T ++/\;;\;\R (iS)/\;;\;

949: \T Y/[k] :=v\ \} $ \\

950: \>\>\>\>~~\B end /\ra\ ;\\

951: \>\>\> $\B else /\; n\T ++/\; \B\ end / $ ;\\

952: \>\> $ \B until /\;\S suc/\Lor a=\S ADR/(r)$ ;\\

953: 41: \>\> $ \B if /\; \S suc/\; \B\ then /\; 

954: h.\T occ/ \T ++/\;\B\ end/$ ;\\

955: 42: \> $ \B return /\; \S suc/$ .

956: \end{tab}

957: 

958: Instruction 35b is a version of compare\&swap. Procedure \S insert/

959: terminates successfully when the insertion to an empty slot is

960: completed, or it fails when there already exists an entry with the

961: given address currently in the hash table (see invariant \S Co3/ and

962: the specification of \S insert/).

963: 

964: \subsubsection{Procedure \S assign/}

965: 

966: Procedure \S assign/ is almost the same as \S insert/ except that 

967: it rewrites an entry with a given value even when the associated 

968: address is not empty. We provide it without further comments.

969: %\newpage

970: \begin {tab}

971: \>$ \B proc /\S assign/ (v:\S Value/\setminus\{\B null/\})

972: \ =$\\

973: \>\>\B local/ $ r:\S EValue/\;;\; k,l,n:\S Nat/\;;\;

974: h:\B pointer to /\S Hashtable/ $ ;\\

975: \>\>\> $ \S suc/:\S Bool/\;;\; a:\S Address/:=\S ADR/(v) $ ;\\

976: 43: \>\>$h:=\T H/[\S index/]\;;\; \S cnt/:=0$;\\

977: 44: \>\> $\B if /\; h.\T occ/> h.\T bound/\;\B\ then /$\\

978: \>\>\> $ \S newTable/()$ ;\\

979: 46: \>\>\> $ h:=\T H/[\S index/]\;\B\ end/$ ;\\

980: 47: \>\> $ n:=0 \;;\; l:=h.\T size/\;;\; \S suc/:= \false $ ;\\

981: \>\>\B repeat/\\

982: 48: \>\>\> $ k:=\; \S key/(a,l,n)$ ;\\

983: 49: \>\>\> $ r:=h.\T table/[k]$ ;\\

984: 50a: \>\>\> $ \B if /\; \S oldp/(r) \;\B\ then/ $\\

985: \>\>\>\> $ \S refresh/()$ ;\\

986: 51: \>\>\>\> $ h:=\T H/[\S index/]$ ;\\

987: 52: \>\>\>\> $n:=0\;;\; l:=h.\T size/$ ;\\

988: \>\>\> $ \B elsif /\; r=\B null/\Lor a=\S ADR/(r) \;

989: \B\ then /$\\

990: 50b: \>\>\>\> \la~$\B if /\;h.\T table/[k] = r\;\B\ then/$\\

991: \>\>\>\>\>$ \S suc/:=\true \;;\;

992: h.\T table/[k] := v\;;\; $\\

993: \>\>\>\>\> $\{\; \S cnt/\T ++/\;;\; \R\ (aS) /;\ \T Y/[k]:=v\ \}$ \\

994: \>\>\>\>~~\B end /\ra \\

995: \>\>\>$ \B else /\; n\T ++/\;\B\ end/$ ;\\

996: \>\> $ \B until /\S suc/ $ ;\\

997: 57: \>\> $ \B if /\; r=\B null/\;\B\ then /\;

998: h.\T occ/\T ++/\;\B\ end/ $ ; \\

999: \>\B end/.

1000: \end{tab}

1001: 

1002: \subsection {Memory management and concurrent migration}

1003: \label{Mem}

1004: 

1005: In this section, we provide the public procedures \S getAccess/ 

1006: and \S releaseAccess/ and the auxiliary procedures \S refresh/ 

1007: and \S newTable/ which are responsible for allocation and 

1008: deallocation. We begin with the treatment of memory by providing 

1009: a model of the heap.

1010: 

1011: \subsubsection {The model of the heap}

1012: We \emph{model} the \T Heap/ as an infinite array of 

1013: hash tables, declared and initialized in the following way:

1014: \begin{tab}

1015: \>\+ $\T Heap/:\B\ array /\S Nat/\B\ of /\S Hashtable/:=([\S Nat/]\bot)$ ;\\

1016: $ \T H/_-\T index/:\S Nat/:= 1 $ .

1017: \end{tab}

1018: So, initially, $\T Heap/[i] = \bot$ for all indices $i$. 

1019: The indices of array \T Heap/ are the pointers to hash tables. We 

1020: thus simply regard \B pointer to/ \S Hashtable/ as a synonym of 

1021: \S Nat/. 

1022: Therefore, the notation $h.\T table/$ used elsewhere in the paper 

1023: stands for $\T Heap/[h].\T table/$. Since we reserve 0 (to be 

1024: distinguished from the absent hash table $\bot$ and the absent 

1025: value \B null/) for the null pointer (i.e. $\T Heap/[0]=\bot$, 

1026: see invariant \S He1/), we initialize \T H/$_-$\T index/, which is 

1027: the index of the next hash table, to be 1 instead of 0. Allocation 

1028: of memory is modeled in

1029: \begin{tab}

1030: \>\+\+ $ \B proc /\S allocate/(s, b:\S Nat/): \S Nat/ =$ \\

1031: \la~$\T Heap/ [\T H/_-\T index/]:=\R\ blank hash table with /

1032: \T size/= s, \T bound/=b,$\\

1033: \>\>\>\> $ \T occ/=\T dels/=0$ ;\\

1034: ~~$\T H/_-\T index/\T ++/\ \ra $ ;\-\\

1035: $\B return /\T H/_-\T index/ $ ;

1036: \end{tab}

1037: We assume that $\S allocate/$ sets all values in the hash table 

1038: $\T Heap/[\T H/_-\T index/]$ to $\B null/$, and also sets its fields 

1039: $\T size/$ and $\T bound/$ as specified. 

1040: The variables \T occ/ and \T dels/ are set to 0 because 

1041: the hash table is completely filled with the value \B null/.

1042:  

1043: Deallocation of hash tables is modeled by

1044: \begin{tab}

1045: \>\+ $ \B proc /\S deAlloc/(h:\S Nat/) =$ \\

1046: \>\la~$ \B assert /\T Heap/[h]\ne\bot\;;\quad

1047: \T Heap/[h]:=\bot\ \ra $ \\

1048: \B end/ .

1049: \end{tab}

1050: The \B assert/ here indicates the obligation to prove 

1051: that \S deAlloc/ is called only for allocated memory.

1052: 

1053: \subsubsection{Procedure \S getAccess/}

1054: The procedure \S getAccess/ is defined as follows.

1055: %\newpage

1056: \begin {tab}

1057: \>$\B proc /\S getAccess/() = $ \\

1058: \>\>$ \B loop/$\\

1059: 59: \>\>\> $ \S index/ :=\; \T currInd/$;\\

1060: 60: \>\>\> $ \T prot/[\S index/]\T ++/$ ;\\

1061: 61: \>\>\> $ \B if / \; \S index/ =\T currInd/\; \B\ then /$\\

1062: 62: \>\>\>\> $ \T busy/[\S index/]\T++/ $ ;\\

1063: 63: \>\>\>\> $ \B if /\; \S index/ =\T currInd/\; 

1064: \B\ then return/ $ ;\\

1065: \>\>\>\> $ \B else /\; \S releaseAccess/(\S index/)\;\B\ end/$ ;\\

1066: 65: \>\>\> $ \B else /\;\T prot/[\S index/]\T --/\;\B\ end/$ ;\\

1067: \>\>\B end/\\

1068: \>\B end/.

1069: \end {tab}

1070: This procedure is a bit tricky. When the process reaches line 62,

1071: the \S index/ has been protected not to be used for creating a 

1072: new hash table in the procedure \S newTable/ (see invariants \S pr2/, 

1073: \S pr3/ and \S nT12/).

1074: 

1075: The hash table pointer $\T H/[\S index/]$ must contain the valid 

1076: contents after the procedure \S getAccess/ returns (see invariants 

1077: \S Ot3/, \S He4/). So, in line 62, \T busy/ is increased, 

1078: guaranteeing that the hash table will not inadvertently be destroyed 

1079: (see invariant \S bu1/ and line 69).

1080: Line 63 needs to check the \S index/ again in case that instruction 

1081: 62 has the precondition that the hash table is not valid. Once some 

1082: process gets hold of one hash table after calling \S getAccess/, no 

1083: process can throw it away until the process releases it (see 

1084: invariant \S rA7/). 

1085:  

1086: \subsubsection{Procedure \S releaseAccess/}\label{deallocate}

1087: The procedure \S releaseAccess/ is given by

1088: \begin {tab}

1089: \>$\B proc /\S releaseAccess/(i:1\DOTS 2P) = $\\

1090: \>\>\B local/ $h:\B pointer to /\S Hashtable/$ ;\\

1091: 67: \>\>$ \S h/ :=\; \T H/[i] $ ;\\

1092: 68: \>\>$ \T busy/[i]\T --/$ ;\\

1093: 69: \>\>$\B if /\;\S h/\ne 0\Land \T busy/[i] = 0\; \B\ then/$\\

1094: 70: \>\>\>$\la~\B if /\T H/[i] = h\; \B\ then /\;\T H/[i]:= 0$ ; \ra\\

1095: 71: \>\>\>\>$ \S deAlloc/(h)$ ;\\

1096: \>\>\>~~\B end/ ;\\

1097: \>\> \B end/ ;\\

1098: 72: \>\> $ \T prot/[i]\T --/$ ;\\

1099: \>\B end/.

1100: \end {tab}

1101: The test $h\ne 0$ at 69 is necessary since it is possible that $h=0$ at the 

1102: lines 68 and 69. This occurs e.g. in the following scenario. 

1103: Assume that process $p$ is at line 62 with $\S index/ \ne\T currInd/$, while

1104: the number $i=\S index/$ satisfies $\T H/[i] = 0$ and $\T busy/[i]=0$.

1105: Then process $p$ increments $\T busy/[i]$, calls $\S releaseAccess/(i)$, 

1106: and arrives at 68 with $h=0$.

1107: 

1108: Since \S deAlloc/ in line 71 accesses a shared variable, we have

1109: separated its call from 70.  The counter $\T busy/[i]$ is used to

1110: protect the hash table from premature deallocation. Only if \T

1111: busy/[i]=0, \T H/[i] can be released.  The main problem of the design

1112: at this point is that it can happen that several processes

1113: concurrently execute \S releaseAccess/ for the same value of $i$, with

1114: interleaving just after the decrement of $\T busy/[i]$. Then they all

1115: may find $\T busy/[i]=0$. Therefore, a bigger atomic command is needed

1116: to ensure that precisely one of them sets $\T H/[i]$ to $0$ (line 70)

1117: and calls \S deAlloc/.  Indeed, in line 71, \S deAlloc/ is called only

1118: for allocated memory (see invariant \S rA3/). The counter $\T

1119: prot/[i]$ can be decreased since position $i$ is no longer used by

1120: this process.

1121: 

1122: \subsubsection{Procedure \S newTable/}

1123: 

1124: When the current hash table has been used for some time, some 

1125: actions of the processes may require replacement of this hash 

1126: table. Procedure \S newTable/ is called when the number of 

1127: occupied positions in 

1128: the current hash table exceeds the \T bound/ (see lines 28, 44). 

1129: Procedure \S newTable/ tries to allocate a new hash table as the 

1130: successor of the current one.

1131: If several processes call \S newTable/ concurrently, they need to 

1132: reach consensus on the choice of an index for the next hash table 

1133: (in line 84). A newly allocated hash table that will not be used 

1134: must be deallocated again.

1135: %\newpage

1136: \begin {tab}

1137: \>$\B proc /\S newTable/() = $ \\

1138: \>\>\B local/ $ i:1\DOTS 2P\;;\;b , bb:\S Bool/$ ;\\

1139: 77: \>\> $ \B while/\; \T next/[\S index/] = 0\; \B\ do/ $\\

1140: 78: \>\>\> $ \B choose /i \in 1\DOTS 2P$ ;\\

1141: \>\>\> \la~$b:=(\T prot/[i] = 0) $ ;\\

1142: \>\>\>~~$ \B if /\;b\;\B\ then / 

1143: \T prot/[i]:=1\;\B\ end / \ra $ ;\\

1144: \>\>\> $\B if /\;b\;\B\ then / $ \\

1145: 81: \>\>\>\> $ \T busy/[i]:=1$ ;\\

1146: 82: \>\>\>\> $\B choose /

1147: \S bound/ > \T H/[\S index/].\T bound/-\T H/[\S index/].\T dels/+2P $ ;\\

1148: \>\>\>\> $\B choose /\S size/> \S bound/+2P $ ;\\

1149: \>\>\>\>$\T H/[i] :=\S allocate/(\S size/, \S bound/)\;; $\\

1150: 83: \>\>\>\> $ \T next/[i]:=0 $ ;\\

1151: 84: \>\>\>\> \la~$ bb:=(\T next/[\S index/] = 0)$ ;\\

1152: \>\>\>\>~~$ \B if /\; bb\; \B\ then /\; 

1153: \T next/[\S index/] :=i\ \B\ end /\ra $ ;\\

1154: \>\>\>\>$ \B if /\; \neg bb\; \B\ then /\;

1155: \S releaseAccess/(i)\; \B\ end /$ ;\\

1156: \>\> \B end end/ ;\\

1157: \>\>$\S refresh/()$ ;\\

1158: \>\B end/ .

1159: \end {tab}

1160: In command 82, we allocate a new blank hash table (see invariant 

1161: \S nT8/), of which the \T bound/ is set greater than 

1162: $\T H/[\S index/].\T bound/-\T H/[\S index/].\T dels/+2P$ 

1163: in order to avoid creating a too small hash table (see invariants 

1164: \S nT6/, \S nT7/). 

1165:  

1166: We require the \T size/ of a hash table to be more than 

1167: $\T bound/+2P$ because of the following scenario: $P$ processes find 

1168: ``$h.\T occ/>h.\T bound/$'' at line 28 and call \S newtable/, 

1169: \S refresh/, \S migrate/, \S moveContents/ and \S moveElement/ one 

1170: after the other. 

1171: After moving some elements, all processes but process $p$ sleep at 

1172: line 126 with $b_{\it mE}=\true$ ($b_{\it mE}$ is the local variable 

1173: $b$ of procedure \S moveElement/). Process $p$ continues the 

1174: migration and updates the new current index when the migration 

1175: completes. Then, process $p$ does several insertions to let the 

1176: \T occ/ of the current hash table reach one more than its \T bound/. 

1177: Just at that moment, $P-1$ processes wake up, increase the \T occ/ 

1178: of the current hash table to be $P-1$ more, and return to line 30. 

1179: Since $P-1$ processes insert different values in the hash table, 

1180: after $P-1$ processes finish their insertions, the \T occ/ of the 

1181: current hash table reaches $2P-1$ more than its \T bound/. 

1182: 

1183: It may be useful to make \T size/ larger than $\T bound/ + 2P $ to 

1184: avoid too many collisions, e.g. with a constraint 

1185: $\T size/\geq\alpha\cdot\T bound/$ for some $\alpha >1$.

1186: If we did not introduce \T dels/, every migration would force the 

1187: sizes to grow, so that our hash table would require unbounded space 

1188: for unbounded life time. We introduced \T dels/ to avoid this.

1189: 

1190: Strictly speaking, instruction 82 inspects one shared variable, 

1191: $\T H/[\S index/]$, and modifies three other shared variables, viz. 

1192: $\T H/[i]$, $\T Heap/[\T H/_-\T index/]$, and $\T H/_-\T index/$. 

1193: In general, we split such multiple shared variable accesses in 

1194: separate atomic commands. Here the accumulation is harmless, since 

1195: the only possible interferences are with other allocations at line 

1196: 82 and deallocations at line 71. In view of the invariant \S Ha2/, 

1197: all deallocations are at pointers $h<\T H/_-\T index/$. 

1198: Allocations do not interfere because they contain the 

1199: increment $\T H/_-\T index/$++ (see procedure \S allocate/).

1200: 

1201: The procedure \S newTable/ first searches for a free index $i$, say 

1202: by round robin. We use a nondeterministic choice.

1203: Once a free index has been found, a hash table is allocated and 

1204: the index gets an indirection to the allocated address. Then the 

1205: current index gets a \T next/ pointer to the new 

1206: index, unless this pointer has been set already.

1207: 

1208: The variables $\T prot/[i]$ are used primarily as 

1209: counters with atomic increments and 

1210: decrements. In 78, however, we use an atomic test-and-set 

1211: instruction.

1212: Indeed, separation of this instruction in two atomic

1213: instructions is incorrect, since that would allow

1214: two processes to grab the same index $i$ concurrently.

1215: 

1216: \subsubsection{Procedure \S migrate/}

1217: After the choice of the new hash table, the procedure \S migrate/ 

1218: serves to transfer the contents in the current hash table to the new

1219: hash table by calling a procedure \S moveContents/ and to update the 

1220: current hash table pointer afterwards. Migration is complete when at 

1221: least one of the (parallel) calls to \S migrate/ has terminated.

1222: 

1223: \begin {tab}

1224: \>$ \B proc /\S migrate/() = $ \\

1225: \>\>\B local/ $i:0\DOTS 2P$; $h:\B pointer to /\S Hashtable/\;;\;

1226: b:\S Bool/$ ;\\

1227: 94: \>\>$ i:=\T next/[\S index/]$;\\

1228: 95: \>\> $ \T prot/[i]\T ++/$ ;\\

1229: 97: \>\>$ \B if /\;\S index/\ne\T currInd/\;\B\ then /$\\

1230: 98: \>\>\>$ \T prot/[i]\T --/$ ;\\

1231: \>\> \B else / \\

1232: 99: \>\>\>$ \T busy/[i] \T ++/$ ;\\

1233: 100: \>\>\>$h:=\T H/[i]$ ;\\

1234: 101: \>\>\>$ \B if /\; \S index/=\T currInd/\;\B\ then / $\\

1235: \>\>\>\>$ \S moveContents/(\T H/[\S index/], h) $ ;\\

1236: 103: \>\>\>\>\la~$b:=(\T currInd/=\S index/)$ ;\\

1237: \>\>\>\>~~$\B if /\; b \;\B\ then /\;\T currInd/:=i$ ;

1238: \ $\{\T Y/:=\T H/[\S i/].\T table/\ \}$\\

1239: \>\>\>\>~~$\B end /\ra$ ;\\

1240:  \>\>\>\>$ \B if /\; b\; \B\ then /$ \\

1241: 104: \>\>\>\>\>$ \T busy/[\S index/] \T --/$ ;\\

1242: 105: \>\>\>\>\>$ \T prot/[\S index/] \T --/$ ;\\

1243: \>\>\> \B end end/ ;\\

1244: \>\>\> $\S releaseAccess/(i)$ ;\\

1245: \>\B end end /.

1246: \end {tab}

1247: 

1248: According to invariants \S mi4/ and \S mi5/, it is an invariant that 

1249: $i=\T next/(\S index/)\neq 0$ holds after instruction 94.

1250: 

1251: Line 103 contains a compare\&swap instruction to update the current 

1252: hash table pointer when some process finds that the migration is 

1253: finished while \T currInd/ is still identical to its \S index/, which 

1254: means that $i$ is still used for the next current hash table (see 

1255: invariant \S mi5/). The increments of $\T prot/[i]$ and $\T busy/[i]$ 

1256: here are needed to protect the next hash table. The decrements serve

1257: to avoid memory loss.

1258: 

1259: \subsubsection{Procedure \S refresh/}

1260: In order to avoid that a delayed process starts migration of an old 

1261: hash table, we encapsulate \S migrate/ in \S refresh/ in the 

1262: following way.

1263: \begin {tab}

1264: \>$ \B proc /\S refresh/() = $\\

1265: 90: \>\>$ \B if /\; \S index/\ne\T currInd/\; \B\ then/ $\\

1266: \>\>\>$ \S releaseAccess/(\S index/) $ ;\\

1267: \>\>\>$ \S getAccess/() $ ;\\ 

1268: \>\>$ \B else /\;\S migrate/()\;\B\ end/$ ;\\

1269: \>\B end/.

1270: \end {tab}

1271: When \S index/ is outdated, the process needs to call

1272: \S releaseAccess/ to abandon its hash table and \S getAccess/ to acquire 

1273: the present pointer to the current hash table.

1274: Otherwise, the process can join the migration.

1275: 

1276: \subsubsection{Procedure \S moveContents/}

1277: Procedure \S moveContents/ has to move the contents of 

1278: the current table to the next current table. All processes that 

1279: have access to the table, may also participate in 

1280: this migration. Indeed, they cannot yet use the new table (see invariants 

1281: \S Ne1/ and \S Ne3/). 

1282: We have to take care that delayed actions on the current 

1283: table and the new table are carried out or abandoned correctly 

1284: (see invariants \S Cu1/ and \S mE10/). 

1285: Migration requires that every value in the current table 

1286: be moved to a unique position in the new table (see invariant \S Ne19/).

1287: 

1288: Procedure \S moveContents/ uses a private variable \S toBeMoved/ 

1289: that ranges over sets of locations. The procedure is given by

1290: %\newpage

1291: \begin {tab}

1292: \>$\B proc /\S moveContents/

1293: (\S from/, \S to/: \B pointer to /\S Hashtable/)=$\\

1294: \>\>\B local/ $i:\S Nat/\;;\;b:\S Bool/\;;\; v:\S EValue/ \;;\;

1295: \S toBeMoved/ : \B set/\ \B of/\ \S Nat/$ ;\\

1296: \>\> $ \S toBeMoved/:= \{ 0,\ldots, \S from/.\T size/-1\}$ ;\\

1297: 110: \>\>$ \B while /\; \T currInd/ = \S index/\wedge

1298: \S toBeMoved/ \ne \emptyset \;\B\ do / $\\

1299: 111: \>\>\>\B choose/ $i\in\S toBeMoved/$ ;\\

1300: \>\>\> $ v:=\S from/.\T table/[i]$ ;\\

1301: \>\>\> $ \B if /\; v=\B done/\; \B\ then/$\\

1302: 112: \>\>\>\>$\S toBeMoved/:=\S toBeMoved/-\{i\}$ ;\\

1303: \>\>\>\B else/\\

1304: 114: \>\>\>\>\la~$b:=(v=\S from/.\T table/[i])$ ;\\

1305: \>\>\>\>~~\B if/ $b$ \B then/ $\S from/.\T table/[i]:=

1306: \S old/(\S val/(v))\;\B\ end / \ra$ ;\\

1307:  \>\>\>\>\B if/ $b$ \B then/\\

1308: 116: \>\>\>\>\> $ \B if /\; \S val/(v)\ne \B null/\; 

1309: \B\ then /\; \S moveElement/(\S val/(v),\S to/)\;\B\ end/$ ;\\

1310: 117: \>\>\>\>\>$\S from/.\T table/[i]:=\B done/ $ ;\\

1311: 118: \>\>\>\>\>$\S toBeMoved/:=\S toBeMoved/-\{i\}$ ;\\

1312:  \>\>\B end end end /;\\

1313: \>\B end/ .

1314: \end {tab}

1315: 

1316: Note that the value is tagged as outdated before it is copied

1317: (see invariant \S mC11/). 

1318: After tagging, the value cannot be deleted or assigned until the 

1319: migration has been completed. Tagging must be done atomically, 

1320: since otherwise an interleaving deletion may be lost. When indeed 

1321: the value has been copied to the new hash table, it becomes 

1322: \B done/ in the old hash table in line 117. This has the effect 

1323: that other processes need not wait for this process to complete 

1324: procedure \S moveElement/, but can help with the migration of this 

1325: value if needed.

1326:  

1327: Since the address is lost after being rewritten to \B done/, we 

1328: had to introduce the shared auxiliary hash table \T Y/ to remember

1329: its value for the proof of correctness. This could have been avoided 

1330: by introducing a second tagging bit, say for ``very old''. 

1331: 

1332: The processes involved in the same migration should not 

1333: use the same strategy for choosing $i$ in line 111, 

1334: since it is advantageous that \S moveElement/ is called often with 

1335: different values. They may exchange information: any of 

1336: them may replace its set \S toBeMoved/ by the intersection 

1337: of that set with the set \S toBeMoved/ of another one. 

1338: We do not give a preferred strategy here, one can refer to 

1339: algorithms for the {\it write-all} problem \cite{Jan00,KS97}.

1340: 

1341: \subsubsection{Procedure \S moveElement/}

1342: 

1343: The procedure \S moveElement/ moves a value 

1344: to the new hash table. Note that the value is tagged as 

1345: outdated in \S moveContents/ before \S moveElement/ is called. 

1346: %\newpage

1347: \begin {tab}

1348: \> $\B proc /\S moveElement/(v:\S Value/\setminus\{\B null/\},

1349: \S to/: \B pointer to /\S Hashtable/) = $ \\

1350: \>\>\B local/ $a:\S Address/\;;\; k,m,n:\S Nat/\;;\; 

1351: w:\S EValue/\;;\; b:\S Bool/$ ;\\

1352: 120: \>\>$n:=0\;;\; b:=\false\;;\; a :=\S ADR/(v)\;;\;

1353: m:=\S to/.\T size/$ ;\\

1354: \>\>\B repeat /\\

1355: 121: \>\>\>$k:=\; \S key/(a,m,n)\;;\; 

1356: w:=\S to/.\T table/[k] $ ;\\

1357: \>\>\>\B if/ $w=\B null/$ \B then/\\

1358: 123: \>\>\>\>\la~$b:=(\S to/.\T table/[k] = \B null/) $;\\

1359: \>\>\>\>~~$ \B if /\; b\; \B\ then /\; \S to/.\T table/[k] :=v\ \B\ end /\ra$ ;\\

1360: \>\>\>\B else/ $n\T ++/\;\B\ end/$ ;\\

1361: 125: \>\> $ \B until / \; b\Lor a=\S ADR/(w) \Lor

1362: \T currInd/ \ne \S index/ $ ;\\

1363: 126: \>\> $ \B if /\; b\; \B\ then /\; \S to/.\T occ/\T ++/\;\B\ end/$ \\

1364: \>\B end/ . 

1365: \end {tab}

1366: 

1367: The value is only allowed to be inserted once in the new hash table 

1368: (see invariant \S Ne19/), since otherwise the main property of open 

1369: addressing would be violated. 

1370: In total, four situations can occur in the procedure moveElement:

1371: \begin{itemize}

1372: \item {the current location $k$ contains a value with a different

1373: address. The process increases $n$ to inspect the next location.}

1374: \item {the current location $k$ contains a value with the same 

1375: address. This means that the value has already been copied to the 

1376: new hash table, the process therefore terminates.}

1377: \item {the current location $k$ is an empty slot. The process inserts 

1378: \S v/ and returns. If insertion fails, since another process filled 

1379: the empty slot in between, the search is continued.}

1380: \item {when \S index/ happens to differ from \T currInd/, 

1381: the entire migration has been completed.}

1382: \end{itemize}

1383: 

1384: While the current hash table pointer is not updated yet,

1385: there exists at least one \B null/ entry in the new hash table 

1386: (see invariants \S Ne8/, \S Ne22/ and \S Ne23/), 

1387: hence the local variable $n$ in the 

1388: procedure \S moveElement/ never goes beyond the size of the

1389:  hash table (see invariants \S mE3/ and \S mE8/), 

1390: and the termination is thus guaranteed.

1391: 

1392: \section {Correctness (Safety)} \label{safety}

1393: 

1394: In this section, we describe the proof of safety of the algorithm. 

1395: The main aspects of safety are functional correctness, atomicity, and 

1396: absence of memory loss. 

1397: These aspects are formalized in eight invariants described in 

1398: section \ref{safetymain}. To prove these invariants, we need many 

1399: other invariants. These are listed in Appendix A. In section 

1400: \ref{intuproof}, we sketch the verification of some of the invariants 

1401: by informal means.  

1402: In section \ref{pvs-model}, we describe how the theorem prover PVS is 

1403: used in the verification. As exemplified in \ref{intuproof}, Appendix B 

1404: gives the dependencies between the invariants. 

1405: 

1406: \B Notational Conventions./  

1407: Recall that there are at most $P$ processes with process identifiers 

1408: ranging from 1 up to $P$. We use $p$, $q$, $r$ to range over process 

1409: identifiers, with a preference for $p$. 

1410: Since the same program is executed by all processes, every private

1411: variable name of a process $\ne p$ is extended with the suffix ``.'' +

1412: ``process identifier''. 

1413: We do not do this for process $p$. So, e.g., the value of a private 

1414: variable $x$ of process $q$ is denoted by $x.q$, but the value of

1415: $x$ of process $p$ is just denoted by $x$. In particular, $pc.q$ is the 

1416: program location of process $q$. It ranges over all integer labels used 

1417: in the implementation. 

1418: 

1419: When local variables in different procedures have the same names, 

1420: we add an abbreviation of the procedure name as a subscript to the name. 

1421: We use the following abbreviations: \S fi/ for \S find/, \S del/ for 

1422: \S delete/, \S ins/ for \S insert/, \S ass/ for \S assign/, \S gA/ for 

1423: \S getAccess/, \S rA/ for \S releaseAccess/, \S nT/ for \S newTable/, 

1424: \S mig/ for \S migrate/, \S ref/ for \S refresh/, \S mC/ for 

1425: \S moveContents/, \S mE/ for \S moveElement/. 

1426: 

1427: In the implementation, there are several places where the same 

1428: procedure is called, say \S getAccess/, \S releaseAccess/, etc. 

1429: We introduce auxiliary private variables \S return/, local to such a

1430: procedure, to hold the return location. We add a procedure subscript

1431: to distinguish these variables according to the above convention. 

1432: 

1433: If $V$ is a set, $\sharp V$ denotes 

1434: the number of elements of $V$. If $b$ is a boolean, then $\sharp b =0$ 

1435: when $b$ is false, and $\sharp b = 1$ when $b$ is true. 

1436: Unless explicitly defined otherwise, we always (implicitly) universally 

1437: quantify over addresses $a$, values $v$, non-negative integer numbers 

1438: $k$, $m$, and $n$, 

1439: natural number $l$, processes $p$, $q$ and $r$. Indices $i$ and $j$ 

1440: range over $[1,2P]$. We abbreviate \T H/(\T currInd/).\T size/ as 

1441: \S curSize/.

1442: 

1443: In order to avoid using too many parentheses, we use the usual binding 

1444: order for the operators. We give ``$\wedge$'' higher priority than

1445: ``$\vee$''. We use parentheses whenever necessary.

1446: 

1447: \subsection {Main properties}\label{safetymain}

1448: 

1449: We have proved the following three safety properties of the algorithm.

1450: Firstly, the access procedures \S find/, \S delete/, \S insert/,

1451: \S assign/, are functionally correct. Secondly they are executed 

1452: atomically. The third safety property is absence of memory loss.

1453: 

1454: Functional correctness of \S find/, \S delete/, \S insert/ is the 

1455: condition that the result of the implementation is the same as the 

1456: result of the specification (fS), (dS), (iS). This is expressed by 

1457: the required invariants:

1458: \begin{tab} %Correct1, Correct2, Correct3\\

1459: \S Co1:/ \>$ \S pc/=14 \Implies \S val/(r_{\it fi})=rS_{\it fi}$ \\

1460: \S Co2:/ \>$ \S pc/\in \{25,26\} \Implies  

1461: suc_{\it del}=sucS_{\it del}$ \\

1462: \S Co3:/ \>$ \S pc/\in \{41,42\} \Implies  

1463: suc_{\it ins}=sucS_{\it ins}$

1464: \end{tab}

1465: 

1466: Note that functional correctness of \S assign/ holds trivially since it

1467:  does not return a result.

1468: 

1469: According to the definition of atomicity in chapter 13 of \cite{Lyn96},

1470: atomicity means that each execution of one of the access procedures

1471: contains precisely one execution of the corresponding specifying action

1472: (fS), (dS), (iS), (aS). We introduced the private auxiliary variables

1473: \S cnt/ to count the number of times the specifying action is executed.

1474: Therefore, atomicity is expressed by the invariants:

1475: \begin{tab}

1476: %\\ ! G-FiCnt1!\\

1477: \S Cn1:/ \>$ \S pc/=14 \Implies \S cnt/_{\it fi}=1 $\\

1478:  %\\ ! G-DeCnt1!\\

1479: \S Cn2:/ \>$ \S pc/\in\{25,26\} \Implies \S cnt/_{\it del}=1 $\\

1480:  %\\ ! G-InCnt1!\\

1481: \S Cn3:/ \>$ \S pc/\in\{41,42\} \Implies \S cnt/_{\it ins}=1 $\\

1482: %\\ ! G-AsCnt1!\\

1483: \S Cn4:/ \>$ \S pc/=57 \Implies \S cnt/_{\it ass}=1 $

1484: \end{tab} 

1485: 

1486: We interpret absence of memory loss to mean that the number of 

1487: allocated hash tables is bounded. More precisely, we prove that 

1488: this number is bounded by $2P$. This is formalized in the invariant:

1489: \begin{tab} % NoLoss

1490: \S No1:/ \>$ \sharp \{k \mid k < \T H/_-\T index/\Land 

1491: \T Heap/(k)\neq\bot\}\leq 2P$ 

1492: \end{tab}

1493: 

1494: An important safety property is that no

1495: process accesses deallocated memory. Since most procedures perform

1496: memory accesses, by means of pointers that are local variables, the

1497: proof of this is based on a number of different invariants. Although,

1498: this is not explicit in the specification, it has been checked 

1499: because the theorem prover PVS does not allow access to

1500: deallocated memory as this would violate type correctness conditions.

1501: 

1502: \subsection{Intuitive proof}\label{intuproof}

1503: 

1504: The eight correctness properties (invariants) mentioned above have 

1505: been completely proved with the interactive proof checker of PVS. 

1506: The use of PVS did not only take care of the delicate bookkeeping 

1507: involved in the proof, it could also deal with many trivial cases 

1508: automatically. At several occasions where PVS refused to let a proof 

1509: be finished, we actually found a mistake and

1510:  had to correct previous versions of this algorithm.

1511: 

1512: In order to give some feeling for the proof, we describe some proofs. 

1513: For the complete mechanical proof, 

1514: we refer the reader to \cite{HesMv}. Note that, for simplicity, we 

1515: assume that all non-specific private variables in the proposed 

1516: assertions belong to the general process $p$, and general process $q$ 

1517: is an active process that tries to 

1518: threaten some assertion ($p$ may equal $q$).\\

1519: 

1520: \noindent \B Proof/ of invariant \S Co1/ (as claimed in 

1521: \ref{safetymain}). According to Appendix B, the 

1522: stability of \S Co1/ follows from the invariants \S Ot3/, \S fi1/,

1523: \S fi10/, which are given in Appendix A. 

1524: Indeed, \S Ot3/ implies that no procedure returns to location 14. 

1525: Therefore all return statements falsify the antecedent of \S Co1/ and 

1526: thus preserve \S Co1/. Since $r_{\it fi}$ and $rS_{\it fi}$ are 

1527: private variables to process $p$, \S Co1/ can only be violated by 

1528: process $p$ itself (establishing $\S pc at 14/$) when $p$ executes 13 

1529: with $r_{\it fi}=\B null/\Lor a_{\it fi}=\S ADR/(r_{\it fi})$. This 

1530: condition is abbreviated as $\S Find/(r_{\it fi},a_{\it fi})$. 

1531: Invariant \S fi10/ then implies that action 13 has the precondition 

1532: $\S val/(r_{\it fi})=rS_{\it fi}$, so then it does not violate 

1533: \S Co1/. In PVS, we used a slightly different definition of \S Find/, 

1534: and we applied invariant \S fi1/ to exclude that $r_{\it fi}$ is 

1535: \B done/ or \B del/, though invariant \S fi1/ is superfluous 

1536: in this intuitive proof.\qed \\

1537: 

1538: \noindent \B Proof/ of invariant \S Ot3/. Since the procedures 

1539: \S getAccess/, \S releaseAccess/, \S refresh/, \S newTable/ are 

1540: called only at specific locations in the algorithm, it is easy to 

1541: list the potential return addresses. Since the variables \S return/ 

1542: are private to process $p$, they are not modified by other processes. 

1543: Stability of \S Ot3/ follows from this. 

1544: As we saw in the previous proof, \S Ot3/ is used to 

1545: guarantee that no unexpected jumps occur.\qed \\

1546: 

1547: \noindent \B Proof/ of invariant \S fi10/. According to Appendix B, 

1548: we only need to use \S fi9/ and \S Ot3/. Let us use the abbreviation 

1549: $k = \S key/(a_{\it fi},l_{\it fi},n_{\it fi})$. Since $r_{\it fi}$ and 

1550: $rS_{\it fi}$ are both private variables, they can only be modified by 

1551: process $p$ when $p$ is executing statement 7. We split this situation 

1552: into two cases

1553: \begin{enumerate}

1554: \item with precondition $\S Find/(h_{\it fi}.\T table/[k],a_{\it fi})$\\

1555: After execution of statement 7,  $r_{\it fi}$ becomes $h_{\it fi}.

1556: \T table/[k]$, 

1557: and $rS_{\it fi}$ becomes $\T X/(a_{\it fi})$. By \S fi9/, we get 

1558: $\S val/(r_{\it fi})=rS_{\it fi}$. Therefore the validity of \S fi10/ 

1559: is preserved.

1560: \item otherwise.\\

1561: After execution of statement 7, $r_{\it fi}$ becomes 

1562: $h_{\it fi}.\T table/[k]$, 

1563: which then falsifies the antecedent of \S fi10/. \qed \\

1564: \end{enumerate}

1565: 

1566: \noindent \B Proof/ of invariant \S fi9/. According to Appendix B, we 

1567: proved that \S fi9/ follows 

1568: from \S Ax2/, \S fi1/, \S fi3/, \S fi4/, \S fi5/, \S fi8/, 

1569: \S Ha4/, \S He4/, \S Cu1/, \S Cu9/, \S Cu10/, and \S Cu11/.

1570: We abbreviate $\S key/(a_{\it fi},l_{\it fi},n_{\it fi})$ as $k$.

1571: We deduce $h_{\it fi}=\T H/(\S index/)$ from \S fi4/, 

1572: $\T H/(\S index/)$ is not 

1573: $\bot$ from \S He4/, and  $k$ is below $\T H/(\S index/).\T size/$ from 

1574: \S Ax2/, \S fi4/ and \S fi3/. We split the proof into two cases:

1575: 

1576: \begin{enumerate}

1577: \item $\S index/\neq\T currInd/$: By \S Ha4/, it follows that 

1578: $\T H/(\S index/)\neq\T H/(\T currInd/)$. Hence from \S Cu1/, we obtain 

1579: $h_{\it fi}.\T table/[k]=\B done/$, which falsifies the antecedent of 

1580: \S fi9/. 

1581: \item $\S index/=\T currInd/$: 

1582: By premise $\S Find/(h_{\it fi}.\T table/[k],a_{\it fi})$, we know that 

1583: $h_{\it fi}.\T table/[k]\neq\B done/$ because of \S fi1/. By \S Cu9/ 

1584: and \S Cu10/, we obtain 

1585: $\S val/(h_{\it fi}.\T table/[k])=\S val/(\T Y/[k])$. 

1586: Hence it follows that $\S Find/(\T Y/[k],a_{\it fi})$. Using \S fi8/, 

1587: we obtain 

1588: \begin{tab}

1589: \>$\forall m<n_{\it fi}:

1590: \neg \S Find/(\T Y/[\S key/(a_{\it fi},\S curSize/,m)],a_{\it fi})$ 

1591: \end{tab}

1592: We get $n_{\it fi}$ is below $\S curSize/$ because of \S fi5/. 

1593: By \S Cu11/, we conclude 

1594: \begin{tab}

1595: \>$\T X/(a_{\it fi})= \S val/(h_{\it fi}.\T table/[k])$ 

1596: \end{tab}

1597: \vspace{-5mm}\qed \\

1598: \end{enumerate}

1599: 

1600: \subsection {The model in PVS} \label{pvs-model}

1601: 

1602: Our proof architecture (for one property) can be described as a 

1603: dynamically growing tree in which each node is associated with an 

1604: assertion. We start from a tree containing only one node, the proof 

1605: goal, which characterizes some property of the system. We expand 

1606: the tree by adding some new children via proper analysis of an 

1607: unproved node (top-down approach, which requires a good understanding 

1608: of the system). The validity of that unproved node is then reduced to 

1609: the validity of its children and the validity of 

1610: some less or equally deep nodes.

1611: 

1612: Normally, simple properties of the system are proved with appropriate 

1613: precedence, and then used to help establish more complex ones. It is 

1614: not a bad thing that some property that was taken for granted turns 

1615: out to be not valid. Indeed, it may uncover a defect of the algorithm, 

1616: but in any case it leads to new insights in it. 

1617: 

1618: We model the algorithm as a transition system \cite{ZA92}, 

1619: which is described in the language of PVS in the following way. 

1620: As usual in PVS, states are represented by a record with a number 

1621: of fields:

1622: {\small

1623: \begin{tab}

1624: \>  State : TYPE = $[\#$ \\

1625: \>  \% \=global variables\\

1626: \>       \>...\\

1627: \>       \>busy : [ range(2*P) $\rightarrow$ nat ],\\

1628: \>       \>prot : [ range(2*P) $\rightarrow$ nat ],\\

1629: \>       \>...\\

1630: \>  \% private variables:\\

1631: \>       \>index : [ range(P) $\rightarrow$ range(2*P) ],\\

1632: \>       \>...\\

1633: \>       \>pc : [ range(P) $\rightarrow$ nat ], \% private program counters\\

1634: \>       \>...\\

1635: \>  \% local variables of procedures, also private to each process:\\

1636: \>  \% find     \\

1637: \>       \>a$_-$find : [ range(P) $\rightarrow$ Address ],\\

1638: \>       \>r$_-$find : [ range(P) $\rightarrow$ EValue ],\\

1639: \>       \>...\\

1640: \>  \% getAccess   \\

1641: \>       \>return$_-$getAccess : [ range(P) $\rightarrow$ nat ],\\

1642: \>       \>...\\

1643: \>  \#]

1644: \end{tab}}

1645: \noindent where \S range/(\R P/) stands for the range 

1646: of integers from 1 to P.

1647: 

1648: Note that private variables are given with as argument a process 

1649: identifier. Local variables are distinguished by adding their 

1650: procedure's names as suffixes.

1651: 

1652: An action is a binary relation on states: it relates the state 

1653: prior to the action to the state following the action. The system 

1654: performed by a particular process is then specified by defining the 

1655: precondition of each action as a predicate on the state and also the 

1656: effect of each action in terms of a state transition. For example, 

1657: line 5 of the algorithm is described in PVS as follows:

1658: {\small

1659: \begin{tab} 

1660: \>\% corresponding to statement find5: $h:=\T H/[\S index/]$; $ n:=0 $;\\  

1661: \>find5(\=i,s1,s2) : bool = \\

1662: \>\>pc(s1)(i)=5 AND\\

1663: \>\>s2 = s1 WITH [ \=(pc)(i) := 6,\\

1664: \>\>\>(n$_-$find)(i) := 0,\\

1665: \>\>\>(h$_-$find)(i) := H(s1)(index(s1)(i)) ]

1666: \end{tab}}

1667: \noindent

1668: where $i$ is a process identifier, s1 is a pre-state, s2 

1669: is a post-state. 

1670: 

1671: Since our algorithm is concurrent, the global transition relation is 

1672: defined as the disjunction of all atomic actions.

1673: {\small

1674: \begin{tab} 

1675: \>\% transition steps \\

1676: \>step(\=i,s1,s2) : bool = \\

1677: \>\> find5(i,s1,s2) or find6(i,s1,s2) or ... \\

1678: \>\> delete15(i,s1,s2) or  delete16(i,s1,s2) or ...\\

1679: \>\>...

1680: \end{tab}}

1681: \noindent

1682: Stability for each invariant is proved by a PVS \S Theorem/ of the form:

1683: {\small

1684: \begin{tab} 

1685: \>\% Theorem about the stability of invariant fi10 \\

1686: \>IV$_-$fi10: THEOREM \\

1687: \>\> forall (u,v : state, q : range(P) ) : \\

1688: \>\>\>  step(q,u,v) AND fi10(u) AND fi9(u) AND ot3(u) \\

1689: \>\>\>  =$>$ fi10(v)

1690: \end{tab}}

1691: \noindent

1692: To ensure that all proposed invariants are stable, there is a 

1693: global invariant \T INV/, which is the conjunction of all proposed invariants.

1694: {\small

1695: \begin{tab} 

1696: \>\% global invariant \\

1697: \>INV(s:state) : bool = \\

1698: \>\> He3(s) and He4(s) and Cu1(s) and ... \\

1699: \>\>...

1700: \end{tab}

1701: \begin{tab} 

1702: \>\% Theorem about the stability of the global invariant INV \\

1703: \>IV$_-$INV: THEOREM \\

1704: \>\> forall (u,v : state, q : range(P) ) : \\

1705: \>\>\>  step(q,u,v) AND INV(u)  =$>$ INV(v)

1706: \end{tab}}

1707: \noindent

1708: We define \T Init/ as all possible initial states, for which all 

1709: invariants must be valid.

1710: {\small 

1711: \begin{tab} 

1712: \>\% initial state \\

1713: \>Init: \{ s : state $\mid$ \\

1714: \>\>\>(forall (p: range(P)):\\

1715: \>\>\>\>  pc(s)(p)=0 and ...\\

1716: \>\>\>\>  ...) and\\

1717: \>\>\>(forall (a: Address):\\

1718: \>\>\>\>  X(s)(a)=null) and \\

1719: \>\>\>...\\

1720: \>\>\>   \}

1721: \end{tab}

1722: \begin{tab} 

1723: \>\% The initial condition can be satisfied by the global invariant 

1724: INV \\

1725: \>IV$_-$Init: THEOREM \\

1726: \>\> INV(Init) 

1727: \end{tab}}

1728: \noindent

1729: The PVS code contains ll

1730: preconditions to imply well-definedness:

1731: e.g. in \S find7/, the hash table must be non-NIL and $\ell$ 

1732: must be its size. 

1733: {\small 

1734: \begin{tab} 

1735: \>\% corresponding to statement find7\\  

1736: \>find7(\=i,s1,s2) : bool = \\

1737: \>\>  i?(Heap(s1)(h$_-$find(s1)(i))) and\\

1738: \>\>  l$_-$find(s1)(i)=size(i$_-$(Heap(s1)(h$_-$find(s1)(i)))) and \\

1739: \>\>  pc(s1)(i)=7 and\\

1740: \>\>  ...

1741: \end{tab}}

1742: 

1743: All preconditions are allowed, since we can prove lock-freedom in 

1744: the following form. In every state $s1$ that satisfies the global 

1745: invariant, every process $q$ can perform a step, i.e., there is a 

1746: state $s2$ with $(s1,s2)\in\S step/$ and 

1747: $\S pc/(s1,q)\ne\S pc/(s2,q)$. This is expressed in PVS by

1748: {\small 

1749: \begin{tab} 

1750: \>\% theorem for lock-freedom\\

1751: \>IV$_-$prog: THEOREM \\

1752: \>\> forall (u: state, q: range(P) ) : \\

1753: \>\>\>  INV(u) =$>$ exists (v: state): pc(u)(q) /= pc(v)(q) and step(q,u,v)

1754: \end{tab}}

1755: 

1756: \section{Correctness (Progress)} \label{progress}

1757: 

1758: In this section, we prove that our algorithm is lock-free, and that 

1759: it is wait-free for several subtasks.

1760: Recall that an algorithm is called {\it lock-free} if always at least 

1761: some process will finish its task in a 

1762: finite number of steps, regardless of delays or failures by other 

1763: processes. This means that no process can block the applications

1764: of further operations to the data structure, although any particular 

1765: operation need not terminate since a slow process can be passed 

1766: infinitely often by faster processes.

1767: We say that an operation is {\it wait-free} if any process involved

1768: in that operation is guaranteed to complete it in a finite number of

1769: its own steps, regardless of the (in)activity of other processes.

1770: 

1771: \subsection {The easy part of progress }

1772: 

1773: It is clear that \S releaseAccess/ is wait-free. It follows that 

1774: the wait-freedom of \S migrate/ depends on wait-freedom of 

1775: \S moveContents/. The loop of \S moveContents/ is clearly bounded. 

1776: So, wait-freedom of \S moveContents/ depends on wait-freedom of 

1777: \S moveElement/. It has been proved that $n$ 

1778: is bounded by $m$ in \S moveElement/ (see invariants \S mE3/ and 

1779: \S mE8/). Since, moreover, $\S to/.\T table/[k]\neq \B null/$ is 

1780: stable, the loop of \S moveElement/ is also bounded. This concludes 

1781: the sketch that \S migrate/ is wait-free. 

1782: 

1783: \subsection {Progress of newTable}

1784: 

1785: The main part of procedure \S newTable/ is wait-free. This can be 

1786: shown informally, as follows. 

1787: Since we can prove the condition $\T next/(\S index/)\neq 0$ is 

1788: stable while process $p$ stays in the region $[77,84]$, once the 

1789: condition $\T next/(\S index/)\neq 0$ 

1790: holds, process $p$ will exit \S newTable/ in a few rounds.

1791: 

1792: Otherwise, we may assume that $p$ has precondition 

1793: $\T next/(\S index/)= 0$ before executing line 78. By the invariant

1794: \begin{tab}

1795: %\\ ! G-next-index1!\\

1796: \S Ne5:/ \>$ pc\in [1,58]\LOR pc\geq 62 \Land pc\neq 65 \Land 

1797: \T next/(\S index/)=0$\\

1798: \> $\implies\quad \S index/=\T currInd/$

1799: \end{tab}

1800: we get that $\S index/ = \T currInd/$ holds and 

1801: $\T next/(\T currInd/)= 0$ from

1802: the precondition. We define two sets of integers:

1803: \begin{tab} %G-prot-set-a

1804: \>\+ $ \S prSet1/(i) \IS 

1805: \{r\mid \S index/.r=i \Land pc.r \notin \{0,59,60\}\}$\\

1806: 

1807: %G-prot-set-b

1808: $\S prSet2/(i) \IS 

1809: \{r\mid \S index/.r=i \Land pc.r \in \{104,105\} $\+\+\+\+\+ \\

1810: $\lor~ i_{\it rA}.r=i \Land \S index/.r \neq i \Land pc.r 

1811: \in [67,72] $\\

1812: $\lor~ i_{\it nT}.r=i \Land pc.r \in [81,84]$\\

1813: $\lor~ i_{\it mig}.r=i \Land pc.r \geq 97\;\}$

1814: \end{tab}

1815: and consider the sum 

1816: $\sum_{i=1}^{2P}(\sharp (prSet1(i)) ~+~ \sharp (prSet2(i)))$.

1817: While process $p$ is at line $78$, the sum cannot exceed $2P-1$

1818: because there are only $P$ processes around and process $p$

1819: contributes only once to the sum. It then follows from the pigeon 

1820: hole principle that there exists $j\in [1,2P]$ such that 

1821: $\sharp (prSet1(j)) ~+~ \sharp (prSet2(j))=0$

1822: and $j\neq \S index/.p$. By the invariant

1823: \begin{tab} 

1824:  %\\ ! G-prot!\\

1825: \S pr1:/\> $ \T prot/[j] = \sharp (\S prSet1/(j)) + 

1826: \sharp (\S prSet2/(j)) +

1827:  \sharp (\T currInd/=j)$\\

1828: \>\>\>\> $ + \sharp (\T next/(\T currInd/)=j)$ 

1829: \end{tab} 

1830: we can get that $\T prot/[j]=0$ because of 

1831: $j\neq \S index/.p = \T currInd/$. 

1832: 

1833: While \T currInd/ is constant, no process can modify $\T prot/[j]$ for 

1834: $j\neq \T currInd/$ infinitely often. Therefore, if process $p$ acts 

1835: infinitely often and chooses its value $i$ in 78 by round robin, 

1836: process $p$ exits the loop of \S newTable/ eventually. This shows 

1837: that the main part of \S newTable/ is wait-free.

1838: 

1839: \subsection{The failure of wait-freedom}

1840: Procedure \S getAccess/ is not wait-free. When the active clients 

1841: keep changing the current index faster than the new client can 

1842: observe it, the accessing client is doomed to starvation. In that case,

1843: however, the other processes repeatedly succeed. It follows that 

1844: \S getAccess/, \S refresh/, and \S newTable/ are lock-free. 

1845: 

1846: It may be possible to make a queue for the accessing clients which 

1847: is emptied by a process in \S newTable/. The accessing clients 

1848: must however also be able to enter autonomously. This would at 

1849: least add another layer of complications. We therefore prefer 

1850: to treat this failure of wait-freedom as a performance issue that

1851: can be dealt with in practice by tuning the sizes of the hash tables. 

1852: 

1853: According to the invariants \S fi5/, \S de8/, \S in8/ and \S as6/, 

1854: the primary procedures \S find/, \S delete/, \S insert/, 

1855: \S assign/ are loops bounded by $n \leq h.\T size/$, and $n$ is only 

1856: reset to 0 during migration. If $n$ is not reset to 0, it is 

1857: incremented or stays constant. Indeed, the atomic \B if/ statements 

1858: in 18b, 35b, and 50b have no \B else/ parts. In \S delete/ and 

1859: \S assign/, it is therefore possible that $n$ stays constant without 

1860: termination of the loop. Since 

1861: \S assign/ can modify non-\B null/ elements of the table, it follows 

1862: that \S delete/ and \S assign/ are not wait-free. 

1863: This unbounded fruitless activity is possible only when \S assign/ 

1864: actions of other processes repeatedly succeed. It follows that the 

1865: primary procedures are lock-free. This concludes the 

1866: argument that the system is lock-free. 

1867: 

1868: \section {Conclusions} \label{conclusions}

1869: 

1870: Lock-free shared data objects are inherently 

1871: resilient to halting failures and permit maximum parallelism. We 

1872: have presented a new practical, lock-free algorithm for 

1873: concurrently accessible hash tables, which promises more robust 

1874: performance and reliability than a conventional lock-based 

1875: implementation. Moreover, the new algorithm is dynamic in the sense 

1876: that it allows the hash table to grow and shrink as needed. 

1877: 

1878: The algorithm scales up linearly with the number of

1879: processes, provided the function {\it key} and the selection

1880: of $i$ in line 111 are defined well. This is confirmed by some

1881: experiments where random values were stored, retrieved

1882: and deleted from the hash table. These experiments indicated 

1883: that $10^6$ insertions, deletions and finds per second and per 

1884: processor are possible on an SGI powerchallenge with 250Mhz R12000 

1885: processors. This figure should only be taken as a rough indicator, 

1886: since the performance of parallel processing is very much influenced

1887: by the machine architecture, the relative sizes of data structures

1888: compared to sizes of caches, and even the scheduling of processes

1889: on processors.

1890: 

1891: The correctness proof for our algorithm is noteworthy because of the 

1892: extreme effort it took to finish it. Formal deduction by 

1893: human-guided theorem proving can, in principle, verify any correct 

1894: design, but doing so may require unreasonable amounts of effort, 

1895: time, or skill. Though PVS provided great help for managing and 

1896: reusing the proofs, we have to admit that the verification for our 

1897: algorithm was very complicated due to the complexity of our 

1898: algorithm. The total verification effort can roughly be estimated 

1899: to consist of two man year excluding the effort in determining the 

1900: algorithm and writing the documentation. The whole proof contains 

1901: around 200 invariants. It takes an 1Ghz Pentium IV computer around 

1902: two days to re-run an individual proof for one of the biggest 

1903: invariants. Without suitable tool support like PVS, we even doubt 

1904: if it would be possible to complete a 

1905: reliable proof of such size and complexity.

1906: 

1907: It may well be possible to simplify the proof and reduce the number 

1908: of invariants slightly, but we did not work on this. The complete 

1909: version of the PVS specifications and the whole proof scripts can 

1910: be found at \cite{HesMv}. Note that we simplified some definitions 

1911: in the paper for the sake of presentation.\\

1912: 

1913: \appendix 

1914: \section{Invariants} \label{Inv}

1915: We present here all invariants whose validity has been verified 

1916: by the theorem prover PVS.

1917: 

1918: \newenvironment{tab1}{\begin{tabbing}

1919: MMMa\=aaa\=aaa\=aaa\=aaa\=aaa\=aaa\= \kill}{\end{tabbing}}

1920: \medbreak Conventions. We abbreviate

1921: \begin {tab1}

1922: \>$\S Find/(\T r/,\T a/)\triangleq ~\T r/=\B null/\Lor \T a/=\S ADR/(\T r/)$ \\

1923: \>$\S LeastFind/(a,n)\triangleq ~$\=$~(\forall m<n:\neg \S Find/(\T Y/[\S key/(a,\S curSize/,m)],a))$\\

1924: \>\>$\land~\S Find/(\T Y/[\S key/(a,\S curSize/,n)],a))$\\

1925: \> $\S LeastFind/(h,a,n)\triangleq ~$\=$~(\forall m<n:\neg \S Find/(h.\T table/[\S key/(a,h.\T size/,m)],a))$\\

1926: \>\>$\land~\S Find/(h.\T table/[\S key/(a,h.\T size/,n)],a))$

1927: \end {tab1}

1928: 

1929: \medbreak Axioms on functions \S key/ and \S ADR/

1930: \begin{tab1} 

1931: %\\ ! ADRjective!\\

1932: \S Ax1:/ \>$ v=\B null/\EQ \S ADR/(v)=\B 0/$ \\

1933: %\\ ! KEYinRange!\\

1934: \S Ax2:/ \>$ 0\leq \S key/(a,l,k) < l$\\

1935: %\\ ! KEYdifferent!\\

1936: \S Ax3:/ \>$ 0\leq k < m < l ~\implies \quad \S key/(a,l,k)\neq \S key/(a,l,m)$

1937: \end{tab1}

1938: 

1939: \medbreak Main correctness properties

1940: \begin{tab1} 

1941: %\\ ! Correct1!\\

1942: \S Co1:/ \>$ pc=14 ~\implies \quad \S val/(r_{\it fi})=rS_{\it fi}$ \\

1943: %\\ ! Correct2!\\

1944: \S Co2:/ \>$ pc\in \{25,26\} ~\implies \quad  suc_{\it del}=sucS_{\it del}$ \\

1945: %\\ ! Correct3!\\

1946: \S Co3:/ \>$ pc\in \{41,42\} ~\implies \quad  suc_{\it ins}=sucS_{\it ins}$\\

1947: %\\ ! G-FiCnt1!\\

1948: \S Cn1:/ \>$ pc=14 ~\implies \quad cnt_{\it fi}=1 $\\

1949:  %\\ ! G-DeCnt1!\\

1950: \S Cn2:/ \>$ pc\in\{25,26\} ~\implies \quad cnt_{\it del}=1 $\\

1951:  %\\ ! G-InCnt1!\\

1952: \S Cn3:/ \>$ pc\in\{41,42\} ~\implies \quad cnt_{\it ins}=1 $\\

1953: %\\ ! G-AsCnt1!\\

1954: \S Cn4:/ \>$ pc=57 ~\implies \quad cnt_{\it ass}=1 $

1955: \end{tab1} 

1956: The absence of memory loss is shown by

1957: \begin{tab1}

1958: %\\ ! NoLoss!\\

1959: \S No1:/ \>$ \sharp (nbSet1) \leq 2*P$ \\

1960: %\\ ! NoLoss1!\\

1961: \S No2:/ \>$ \sharp (nbSet1)=\sharp (nbSet2)$

1962: \end{tab1}

1963: where $nbSet1$ and $nbSet2$ are sets of integers, characterized by

1964: \begin{tab1} 

1965: %\\ ! H-nonbot!\\

1966: $\S nbSet1/ \IS \{k \mid k < \T H/_-\T index/\Land \T Heap/(k)\neq\bot\}$\\

1967: 

1968: %\\ ! H-nonbot1!\\

1969: $\S nbSet2/ \IS 

1970: \{i\mid \T H/(i)\neq 0 \lor (\exists r:pc.r=71 \land i_{\it rA}.r=i)\}$

1971: \end{tab1}

1972: 

1973: 

1974: \medbreak Further, we have the following definitions of sets of integers:

1975: 

1976: \begin{tab1}

1977: %\\ ! G-ghostset1!\\

1978: $\S deSet1/ \IS \{k\mid k < \S curSize/\Land \T Y/[k]=\B del/\}$\\

1979: 

1980: %\\ ! G-delset1!\\

1981: $\S deSet2/ \IS \{r\mid \S index/.r=\T currInd/ \Land pc.r=25 \land 

1982: suc_{\it del}.r\}$\\

1983: 

1984: %\\ ! G-delset!\\

1985: $\S deSet3/\IS \{k\mid k < \T H/(\T next/(\T currInd/)).\T size/ $\\

1986: \> $\Land \T H/(\T next/(\T currInd/)).\T table/[k]=\B del/\}$ \\

1987: 

1988: %\\ ! G-occset1!\\

1989: $\S ocSet1/\IS \{r\mid \S index/.r\neq \T currInd/$\\

1990: \>\>$\lor\; pc.r\in [30,41] \Lor pc.r\in [46,57]$\\

1991: \>\>$\lor\; pc.r \in [59,65]\Land return_{\it gA}.r\geq 30$ \\

1992: \>\>$\lor\; $\=$pc.r \in [67,72]\land\; (return_{\it rA}.r=59\Land return_{\it gA}.r\geq 30$\\

1993: \>\>\>\>$\lor\; return_{\it rA}.r=90\Land return_{\it ref}.r\geq 30)$ \\

1994: \>\>$\lor\; (pc.r=90\Lor pc.r\in [104,105])\Land return_{\it ref}.r\geq 30\}$ \\

1995: 

1996: %\\ ! G-occset2!\\

1997: $\S ocSet2/ \IS \{r\mid pc.r \geq 125 \Land b_{\it mE}.r \Land 

1998: to.r=\T H/(\T currInd/)\} $ \\

1999: 

2000: %\\ ! G-occset3!\\

2001: $\S ocSet3/ \IS 

2002: \{r\mid \S index/.r=\T currInd/ \Land pc.r=41 \Land suc_{\it ins}.r$\\

2003: \>\>$\Lor \S index/.r=\T currInd/ \Land pc.r=57\Land  r_{\it ass}.r=\B null/\}$\\

2004: 

2005: %\\ ! G-set1!\\

2006: $\S ocSet4/\IS \{k\mid 

2007: k < \S curSize/ \Land \S val/(\T Y/[k])\neq\B null/\}$\\

2008: 

2009: %\\ ! G-set2!\\

2010: $\S ocSet5/\IS 

2011: \{k\mid k <\T H/(\T next/(\T currInd/)).\T size/ $\\

2012: \>\>$\Land \S val/(\T H/(\T next/(\T currInd/)).\T table/[k])\neq\B null/\}$\\

2013: 

2014: %\\ ! G-nextset!\\

2015: $\S ocSet6/\IS 

2016: \{k\mid k < \T H/(\T next/(\T currInd/)).\T size/ $\\

2017: \>\>$\Land \T H/(\T next/(\T currInd/)).\T table/[k]\neq\B null/\}$\\

2018: 

2019: %\\ ! G-nextset1!\\

2020: $\S ocSet7/\IS \{r\mid  pc.r\geq 125\Land 

2021: b_{\it mE}.r\Land to.r=\T H/(\T next/(\T currInd/))\}$ \\

2022: 

2023: %\\ ! G-prot-set!\\

2024: $ \S prSet1/(i) \IS 

2025: \{r\mid \S index/.r=i \Land pc.r \notin \{0,59,60\}\}$\\

2026: 

2027: %\\ ! G-prot-set!\\

2028: $\S prSet2/(i) \IS 

2029: \{r\mid \S index/.r=i \Land pc.r \in \{104,105\} $\\

2030: \>\>$\lor~ i_{\it rA}.r=i \Land \S index/.r \neq i \Land pc.r 

2031: \in [67,72] $\\

2032: \>\>$\lor~ i_{\it nT}.r=i \Land pc.r \in [81,84]$\\

2033: \>\>$\lor~ i_{\it mig}.r=i \Land pc.r \geq 97\}$\\

2034: 

2035: %\\ ! G-prot-set1!\\

2036: $\S prSet3/(i)\IS 

2037: \{r\mid \S index/.r=i \Land pc.r \in [61,65]\cup [104,105] $\\

2038: \>\>$\lor~ i_{\it rA}.r=i \Land pc.r=72 $\\

2039: \>\>$\lor~ i_{\it nT}.r=i \Land pc.r \in [81,82]$\\

2040: \>\>$\lor~ i_{\it mig}.r=i \Land pc.r \in [97,98]\}$\\

2041: 

2042: %\\ ! G-prot-set2!\\

2043: $\S prSet4/(i) \IS 

2044: \{r\mid \S index/.r=i \Land pc.r \in [61,65] $\\

2045: \>\>$\lor~ i_{\it mig}.r=i \Land pc.r \in [97,98]\}$ \\

2046: 

2047: %\\ ! G-busy-set!\\

2048: $\S buSet1/(i) \IS 

2049: \{r\mid \S index/.r=i$\\

2050: \>\>$\land~ $\=$(pc.r \in [1,58]\cup (62,68]\Land pc.r\neq 65$\\

2051: \>\>\>$\lor~ pc.r\in [69,72] \Land return_{\it rA}.r>59$\\

2052: \>\>\>$\lor~ pc.r>72)\}$ \\

2053: 

2054: %\\ ! G-busy-set!\\

2055: $\S buSet2/(i)\IS 

2056: \{r\mid \S index/.r=i \Land pc.r=104$\\

2057: \>\>$\lor~ i_{\it rA}.r=i \Land \S index/.r \neq i \Land pc.r \in [67,68] $\\

2058: \>\>$\lor~ i_{\it nT}.r=i \Land pc.r \in [82,84]$\\

2059: \>\>$\lor~ i_{\it mig}.r=i \Land pc.r \geq 100\}$

2060: \end{tab1}

2061: 

2062: 

2063: \medbreak We have the following invariants concerning the \T Heap/

2064: \begin{tab1} 

2065: %\\ ! G-H5!\\

2066: \S He1:/ \>$ \T Heap/(0)=\bot$ \\

2067: 

2068: %\\ ! G-H2,G-H4!\\

2069: \S He2:/ \>$ \T H/(i)\neq 0\equiv \T Heap/(\T H/(i))\neq \bot$\\

2070: 

2071: %\\ ! G-k0-a!\\

2072: \S He3:/\>$ \T Heap/(\T H/(\T currInd/))\neq \bot$ \\

2073: 

2074: %\\ ! G-k0-b!\\

2075: \S He4:/\>$ pc \in [1,58] \Lor pc>65 \Land \neg(pc \in [67,72]\Land i_{\it rA}=\S index/)$\\

2076: \>$\implies \quad \T Heap/(\T H/(\S index/))\neq \bot$ \\

2077: 

2078: %\\ ! G-k2!\\

2079: \S He5:/\>$ \T Heap/(\T H/(i))\neq \bot ~\implies \quad\ \T H/(i).\T size/\geq P$\\

2080: 

2081: %\\ ! G-next-currInd4!\\

2082: \S He6:/\>$ \T next/(\T currInd/)\neq 0~\implies \quad

2083: \T Heap/(\T H/(\T next/(\T currInd/)))\neq\bot$ 

2084: \end{tab1}

2085: 

2086: \medbreak Invariants concerning  hash table pointers

2087: \begin{tab1}

2088: %\\ ! G-H-index1!\\

2089: \S Ha1:/ \>$ \T H/_-\T index/>0$ \\

2090: 

2091: %\\ ! G-H-index!\\

2092: \S Ha2:/ \>$ \T H/(i)<\T H/_-\T index/$ \\

2093: 

2094: %\\ ! G-H1!\\

2095: \S Ha3:/ \>$ i\neq j\Land \T Heap/(\T H/(i))\neq \bot ~\implies \quad \T H/(i)\neq\T H/(j)$\\

2096: 

2097: %\\ ! G-index!\\

2098: \S Ha4:/ \>$ \S index/\neq \T currInd/~\implies \quad\ \T H/(\S index/)\neq \T H/(\T currInd/)$ \\

2099: %\>;this can be eliminated by (k0-a) and (H1)

2100: \end{tab1}

2101: 

2102: Invariants about counters for calling the specification.

2103: 

2104: \begin{tab1} 

2105: %\\ ! G-FiCnt3!\\

2106: \S Cn5:/ \>$ pc\in [6,7]~\implies \quad cnt$\=$_{\it fi}=0 $\\

2107: %\\ ! G-FiCnt2!\\

2108: \S Cn6:/ \>$ pc\in [8,13]$\\

2109: \>$\lor~ pc\in [59,65] \land return_{\it gA}=10$\\

2110: \>$\lor~ pc\in [67,72] \land ($\=$return_{\it rA}=59 \land return_{\it gA}=10$\\

2111: \>\>$\lor~ return_{\it rA}=90 \land return_{\it ref}=10$\\

2112: \>$\lor~ pc \geq 90 \Land return_{\it ref}=10$ \\

2113: \>$\implies \quad cnt$\=$_{\it fi}=\sharp (r_{\it fi}=\B null/\lor a_{\it fi}=\S ADR/(r_{\it fi}))$ \\

2114: 

2115:  %\\ ! G-DeCnt2!\\

2116: \S Cn7:/ \>$ pc\in [16,21]\Land pc\neq 18 $\\

2117: \>$\lor~ pc\in [59,65] \land return_{\it gA}=20$\\

2118: \>$\lor~ pc\in [67,72] \land ($\=$return_{\it rA}=59 \land return_{\it gA}=20$\\

2119: \>\>$\lor~ return_{\it rA}=90 \land return_{\it ref}=20$\\

2120: \>$\lor~ pc \geq 90 \Land return_{\it ref}=20$ \\

2121: \>$\implies \quad cnt_{\it del}= 0$\\

2122: 

2123:  %\\ ! G-DeCnt3!\\

2124: \S Cn8:/ \>$ pc=18 ~\implies \quad cnt_{\it del}=\sharp (r_{\it del}=\B null/)$\\

2125: 

2126: %\\ ! G-InCnt3!\\

2127: \S Cn9:/ \>$ pc\in [28,33]$\\

2128: \>$\lor~ pc\in [59,65] \land return_{\it gA}=30$\\

2129: \>$\lor~ pc\in [67,72] \land ($\=$return_{\it rA}=59 \land return_{\it gA}=30$\\

2130: \>\>$\lor~ return_{\it rA}=77 \land return_{\it nT}=30$\\

2131: \>\>$\lor~ return_{\it rA}=90 \land return_{\it ref}=30$\\

2132: \>$\lor~ pc\in [77,84] \land return_{\it nT}=30 $\\

2133: \>$\lor~ pc \geq 90 \Land return_{\it ref}=30$ \\

2134: \>$\implies \quad cnt_{\it ins}= 0$ \\

2135: 

2136: %\\ ! G-InCnt2!\\

2137: \S Cn10:/ \>$ pc\in [35,37]$\\

2138: \>$\lor~ pc\in [59,65] \land return_{\it gA}=36$\\

2139: \>$\lor~ pc\in [67,72] \land ($\=$return_{\it rA}=59 \land return_{\it gA}=36$\\

2140: \>\>$\lor~ return_{\it rA}=90 \land return_{\it ref}=36$\\  

2141: \>$\lor~ pc \geq 90 \Land return_{\it ref}=36$ \\

2142: \>$\implies \quad cnt_{\it ins}= \sharp (a_{\it ins}=\S ADR/(r_{\it ins})\lor suc_{\it ins})$\\

2143: 

2144: %\\ ! G-AsCnt2!\\

2145: \S Cn11:/ \>$ pc\in [44,52]$\\

2146: \>$\lor~ pc\in [59,65] \land return_{\it gA}\in \{46,51\}$\\

2147: \>$\lor~ pc\in [67,72] \land ($\=$return_{\it rA}=59 \land return_{\it gA} \in \{46,51\}$\\

2148: \>\>$\lor~ return_{\it rA}=77 \land return_{\it nT}=46$\\

2149: \>\>$\lor~ return_{\it rA}=90 \land return_{\it ref} \in \{46,51\}$\\  

2150: \>$\lor~ pc\in [77,84] \land return_{\it nT}=46 $\\

2151: \>$\lor~ pc \geq 90 \Land return_{\it ref}\in \{46,51\}$ \\

2152: \>$\implies \quad cnt_{\it ass}sign= 0$

2153: \end{tab1}

2154: 

2155: \medbreak Invariants about old hash tables, current hash table and the auxiliary hash table \T Y/.

2156:  Here, we universally quantify over all non-negative integers $n< \S curSize/$.

2157: \begin{tab1}

2158: %\\ ! G-k1!\\

2159: \S Cu1:/ \>$ \T H/(\S index/)\neq \T H/(\T currInd/)\Land k < \T H/(\S index/).\T size/$\\

2160: \>$\land~ (pc\in [1,58]\Lor pc>65 \Land 

2161: \neg( pc\in[67,72]\Land i_{\it rA}=\S index/)$\\

2162: \>$\implies\quad \T H/(\S index/).\T table/[k]=\B done/$ \\

2163: 

2164: %\\ ! G-ghostocc1!\\

2165: \S Cu2:/ \>$\sharp(\{k\mid k < \S curSize/\Land \T Y/[k]\neq\B null/\})<\S curSize/$ \\

2166: 

2167: %\\ ! G-bound1!\\

2168: \S Cu3:/ \>$ \T H/(\T currInd/).\T bound/+2*P<\S curSize/$\\

2169: 

2170: %\\ ! G-ghostdel1!\\

2171: \S Cu4:/ \>$ \T H/(\T currInd/).\T dels/+\sharp(deSet2)=\sharp(deSet1)$\\

2172: 

2173: %\\ ! G-ghostocc,G-ghostset!\\

2174: \S Cu5:/ \>\S Cu5/ has been eliminated. The numbering has been kept, so as not to\\

2175: \> endanger the consistency with Appendix B and the PVS script.\\

2176: 

2177: %\\ ! G-ghostocc2!\\

2178: \S Cu6:/ \>$ \T H/(\T currInd/).\T occ/+\sharp (ocSet1)+\sharp (ocSet2)\leq\T H/(\T currInd/).\T bound/+2*P$\\

2179: 

2180: %\\ ! G-ghostocc3!\\

2181: \S Cu7:/\>$\sharp(\{k\mid k < \S curSize/\Land\T Y/[k]\neq\B null/\}$ \\

2182: \> $ = \T H/(\T currInd/).\T occ/+\sharp (ocSet2) + \sharp (ocSet3)$\\

2183: 

2184: %\\ ! G-next-currInd3!\\

2185: \S Cu8:/ \>$\T next/(\T currInd/) = 0~\implies \quad

2186: \neg\,\S oldp/(\T H/(\T currInd/).\T table/[n])$\\

2187: 

2188: %\\ ! G-ghost1-a!\\

2189: \S Cu9:/ \>$\neg (\S oldp/(\T H/(\T currInd/).\T table/[n]))~\implies \quad 

2190: \T H/(\T currInd/).\T table/[n]=\T Y/[n] $\\

2191: 

2192: %\\ ! G-ghost1-b!\\

2193: \S Cu10:/ \>$\S oldp/(\T H/(\T currInd/).\T table/[n]) \Land \S val/(\T H/(\T currInd/).\T table/[n])\neq \B null/$\\

2194: \>$\implies\ \S val/(\T H/(\T currInd/).\T table/[n])=\S val/(\T Y/[n])$ \\

2195: 

2196: %\\ ! G-ghost2-a!\\

2197: \S Cu11:/ \>$\S LeastFind/(a,n)~\implies \quad \T X/(a)=\S val/(\T Y/[\S key/(a,\S curSize/,n)])$\\

2198: 

2199: %\\ ! G-ghost2-b!\\

2200: \S Cu12:/ \>$\T X/(a)=\S val/(\T Y/[\S key/(a,\S curSize/,n)]) 

2201: \neq \B null/~\implies \quad \S LeastFind/(a,n)$ \\

2202: 

2203: %\\ ! G-ghost3-a!\\

2204: \S Cu13:/ \>$\T X/(a)=\S val/(\T Y/[\S key/(a,\S curSize/,n)])\neq \B null/

2205: \Land n \ne m < \S curSize/$\\

2206: \>$\implies \quad \S ADR/(\T Y/[\S key/(a,\S curSize/,m)])\neq a $ \\

2207: 

2208: %\\ ! G-ghost3-b!\\

2209: \S Cu14:/ \>$\T X/(a)=\B null/\Land \S val/(\T Y/[\S key/(a,\S curSize/,n)])\neq \B null/$\\

2210: \>$\implies \quad \S ADR/(\T Y/[\S key/(a,\S curSize/,n)])\neq a$ \\

2211: 

2212: %\\ ! G-ghost4!\\

2213: \S Cu15:/ \>$\T X/(a)\neq\B null/$\\

2214: \>$\implies\ \exists m < \S curSize/:\T X/(a)=\S val/(\T Y/[\S key/(a,\S curSize/,m)])$ \\

2215: 

2216: %\\ ! G-ghostbij!\\

2217: \S Cu16:/ \>$\exists (f:[$\=$\{m:0\leq m<\S curSize/)\land \S val/(\T Y/[m])\neq \B null/\}\rightarrow $\\

2218: \>\>$\{v:v\neq\B null/\land (\exists k<\S curSize/:v=\S val/(\T Y/[k]))\}]):$\\

2219: \>$f~ \T is bijective/$ 

2220: \end{tab1}

2221: 

2222: 

2223: \medbreak Invariants about \T next/ and $\T next/(\T currInd/)$:

2224: 

2225: \begin{tab1} 

2226: %\\ ! G-next-currInd!\\

2227: \S Ne1:/ \>$ \T currInd/\neq\T next/(\T currInd/)$\\

2228: 

2229: %\\ ! G-next-currInd1!\\

2230: \S Ne2:/ \>$ \T next/(\T currInd/)\neq 0~\implies \quad\T next/(\T next/(\T currInd/))=0$\\

2231: 

2232:  %\\ ! G-next-currInd2!\\

2233: \S Ne3:/ \>$ pc\in [1,59]\Lor pc\geq 62 \Land pc\neq 65~\implies \quad \S index/\neq\T next/(\T currInd/)$\\

2234: 

2235: %\\ ! G-next-index!\\

2236: \S Ne4:/ \>$ pc\in [1,58]\Lor pc\geq 62 \Land pc\neq 65~\implies \quad \S index/\neq\T next/(\S index/)$\\

2237: 

2238: %\\ ! G-next-index1!\\

2239: \S Ne5:/ \>$ pc\in [1,58]\Lor pc\geq 62 \Land pc\neq 65 \Land \T next/(\S index/)=0$\\

2240: \> $ \implies\quad \S index/=\T currInd/$\\

2241: 

2242: %\\ ! G-ghostocc4!\\

2243: \S Ne6:/ \>$ \T next/(\T currInd/)\neq 0$\\

2244: \>$\implies \quad $\=$ \sharp (\S ocSet6/)\leq \sharp(\{k\mid k < \S curSize/\Land \T Y/[k]\neq\B null/\}-\T H/(\T currInd/).\T dels/$\\

2245: \>\>$-\sharp (deSet2)$\\

2246: 

2247:  %\\ ! G-nextbound1!\\

2248: \S Ne7:/ \>$ \T next/(\T currInd/)\neq 0$\\

2249: \>$\implies \quad $\=$\T H/(\T currInd/).\T bound/-\T H/(\T currInd/).\T dels/+2*P$\\

2250: \>\>$\leq\T H/(\T next/(\T currInd/)).\T bound/$\\

2251: 

2252:  %\\ ! G-nextbound2!\\

2253: \S Ne8:/ \>$ \T next/(\T currInd/)\neq 0$\\

2254: \>$\implies \quad \T H/(\T next/(\T currInd/)).\T bound/+

2255: 2*P<\T H/(\T next/(\T currInd/)).\T size/$\\

2256: 

2257:  %\\ ! G-nextdel!\\

2258: \S Ne9:/ \>$ \T next/(\T currInd/)\neq 0 ~\implies \quad 

2259: \T H/(\T next/(\T currInd/)).\T dels/=\sharp (\S deSet3/)$\\

2260: 

2261:  %\\ ! G-Ne9a!\\

2262: \S Ne9a:/ \>$ \T next/(\T currInd/)\neq 0 ~\implies \quad 

2263: \T H/(\T next/(\T currInd/)).\T dels/=0$ \\

2264: 

2265: %\\ ! G-migrate9!\\

2266: \S Ne10:/ \>$ \T next/(\T currInd/)\neq 0 \Land k < h.\T size/~\implies \quad h.\T table/[k]\notin \{\B del/,\B done/\} $,\\

2267: \>where $h=\T H/(\T next/(\T currInd/))$\\

2268: 

2269: %\\ ! G-migrate4-1!\\

2270: \S Ne11:/ \>$\T next/(\T currInd/)\neq 0\Land 

2271: k < \T H/(\T next/(\T currInd/)).\T size/ $\\

2272: \> $\implies\quad \neg\S oldp/(\T H/(\T next/(\T currInd/)).\T table/[k])$\\

2273: 

2274: %\\ ! G-migrate3-1-a!\\

2275: \S Ne12:/ \>$ k < \S curSize/\Land \T H/(\T currInd/).\T table/[k]=\B done/\Land  m< h.\T size/$\\

2276: \>$\land\;\; \S LeastFind/(h,a,m) $\\

2277: \> $ \implies\quad \T X/(a)=\S val/(h.\T table/[\S key/(a,h.\T size/,m)])$, \\

2278: \> where $a=\S ADR/(\T Y/[k])$ and $h=\T H/(\T next/(\T currInd/)))$\\

2279: 

2280:  %\\ ! G-migrate3-1-b!\\

2281: \S Ne13:/ \>$k < \S curSize/\Land \T H/(\T currInd/).\T table/[k]=\B done/\Land m <h.\T size/$\\

2282: \> $\land\;\; \T X/(a)=\S val/(h.\T table/[\S key/(a,h.\T size/,m)])

2283: \neq \B null/$\\

2284: \> $\implies\quad \S LeastFind/(h,a,m)$,\\

2285: \> where $a=\S ADR/(\T Y/[k])$ and $h=\T H/(\T next/(\T currInd/))$\\

2286: 

2287:  %\\ ! G-migrate3-2!\\

2288: \S Ne14:/ \>$\T next/(\T currInd/)\neq 0 \Land a\neq \B 0/ \Land k < h.\T size/$\\

2289: \>$\land\;\; \T X/(a)=\S val/(h.\T table/[\S key/(a,h.\T size/,k)])

2290: \neq\B null/$\\

2291: \>$\implies\quad \S LeastFind/(h,a,k)$,\\

2292: \>where $h=\T H/(\T next/(\T currInd/))$\\

2293: 

2294:  %\\ ! G-migrate5-1!\\

2295: \S Ne15:/ \>$k < \S curSize/\Land \T H/(\T currInd/).\T table/[k]=\B done/\Land \T X/(a)\neq \B null/$\\

2296: \>$ \land\;\; m < h.\T size/\Land \T X/(a)=\S val/(h.\T table/[\S key/(a,h.\T size/,m)])$\\

2297: \>$ \land\;\; n < h.\T size/ \Land m \ne n $ \\

2298: \> $\implies\quad \S ADR/(h.\T table/.[\S key/(a,h.\T size/,n)])\ne a$,\\

2299: \>where $ a=\S ADR/(\T Y/[k])$ and $h=\T H/(\T next/(\T currInd/))$\\

2300: 

2301: %\\ !  G-migrate5-1!\\

2302: \S Ne16:/ \>$k < \S curSize/\Land \T H/(\T currInd/).\T table/[k]=\B done/\Land \T X/(a)= \B null/ $\\

2303: \>$\land\;\; m < h.\T size/$\\

2304: \>$\implies\quad \S  val/(h.\T table/[\S key/(a,h.\T size/,m)]) = \B null/$\\

2305: \>\>$\lor\;\; \S ADR/(h.\T table/[\S key/(a,h.\T size/,m)])\ne a $, \\

2306: \>where $ a=\S ADR/(\T Y/[k])$ and $h=\T H/(\T next/(\T currInd/))$\\

2307: 

2308: 

2309:  %\\ !  G-migrate5-2!\\

2310: \S Ne17:/ \>$ \T next/(\T currInd/)\neq 0\Land m < h.\T size/\Land a=\S ADR/(h.\T table/[m])\ne 0 $\\

2311: \> $ \implies\quad \T X/(a)=\S val/(h.\T table/[m]) \neq \B null/$, \\

2312: \>where $h=\T H/(\T next/(\T currInd/))$\\

2313: 

2314:  %\\ !  G-migrate5-2!\\

2315: \S Ne18:/ \>$ \T next/(\T currInd/)\neq 0\Land m < h.\T size/\Land a = \S ADR/(h.\T table/[m]) \ne 0 $\\

2316: \> $ \implies\quad \exists n < \S curSize/: \S val/(\T Y/[n])=\S val/(h.\T table/[m]) $\\

2317: \>\>$\land\;\; \S oldp/(\T H/(\T currInd/).\T table/[n])$, \\

2318: \>where $h=\T H/(\T next/(\T currInd/))$\\

2319: 

2320:  %\\ !  G-migrate5-3!\\

2321: \S Ne19:/ \>$ \T next/(\T currInd/)\neq 0 \Land m < h.\T size/ \Land  m \ne n < h.\T size/$ \\

2322: \> $ \land\;\; a = \S ADR/(h.\T table/[\S key/(a,h.\T size/,m)])\ne 0 $\\

2323: \> $ \implies\quad \S ADR/(h.\T table/[\S key/(a,h.\T size/,n)])\ne a $,\\

2324: \>where $h=\T H/(\T next/(\T currInd/))$\\

2325: 

2326:  %\\ !  G-migrate6-4!\\

2327: \S Ne20:/ \>$ k < \S curSize/\Land 

2328: \T H/(\T currInd/).\T table/[k]=\B done/ \Land \T X/(a)\neq \B null/$\\

2329: \>$\implies \quad \exists m < h.\T size/: 

2330: \T X/(a)=\S val/(h.\T table/[\S key/(a,h.\T size/,m)])$,\\

2331: \>where $a=\S ADR/(\T Y/ [k])$ and $ h=\T H/(\T next/(\T currInd/))$\\

2332: 

2333: %\\ ! G-nextocc!\\

2334: \S Ne21:/ \>\S Ne21/ has been eliminated.\\

2335: 

2336: %\\ ! G-nextocc2!\\

2337: \S Ne22:/ \>$ \T next/(\T currInd/)\neq 0~$\\

2338: \>$\implies \quad \sharp (\S ocSet6/)=\T H/(\T next/(\T currInd/)).\T occ/+\sharp (ocSet7)$\\

2339: 

2340: %\\ ! G-nextocc1!\\

2341: \S Ne23:/ \>$ \T next/(\T currInd/)\neq 0~$\\

2342: \>$\implies \quad \T H/(\T next/(\T currInd/)).\T occ/\leq\T H/(\T next/(\T currInd/)).\T bound/$ \\

2343: 

2344: %\\ ! G-nextinj3!\\

2345: \S Ne24:/ \>$ \T next/(\T currInd/)\neq 0~\implies \quad 

2346: \sharp (\S ocSet5/)\leq \sharp (\S ocSet4/)$ \\

2347: 

2348: %\\ ! G-nextbij!\\

2349: \S Ne25:/ \>$~~~ \T next/(\T currInd/)\neq 0$\\

2350: \>$\implies \quad \exists $\=$(f:[$\=$\{m:0\leq m<h.\T size/\land \S val/(h.\T table/[m])\neq \B null/\}\rightarrow $\\

2351: \>\>$\{v:v\neq\B null/\land (\exists k<h.\T size/:v=\S val/(h.\T table/[k]))\}]):$\\

2352: \>\>$f~ \T is bijective/$, \\

2353: \>where $h=\T H/(\T next/(\T currInd/))$\\

2354: 

2355: %\\ ! G-nextinj1!\\

2356: \S Ne26:/ \>$~~~ \T next/(\T currInd/)\neq 0$\\

2357: \>$\implies \quad \exists $\=$(f:[$\=$\{v:v\neq\B null/

2358: \land (\exists m<h.\T size/:v=\S val/(h.\T table/[m]))\}\rightarrow $\\

2359: \>\>\>$\{v:v\neq\B null/\land (\exists k:<\S curSize/:v=\S val/(\T Y/[k]))\}]):$\\

2360: \>\>$f~ \T is injective/$, \\

2361: \>where $h=\T H/(\T next/(\T currInd/))$\\

2362: 

2363: %\\ ! G-nextinj2!\\

2364: \S Ne27:/ \>$~~~ \T next/(\T currInd/)\neq 0 \Land (\exists n<h.\T size/: \S val/(h.\T table/[n])\neq \B null/)$\\

2365: \>$\implies \quad \exists $\=$(f:[$\=$\{m:0\leq m<h.\T size/\land \S val/(h.\T table/[m]) \neq \B null/\} \rightarrow $\\

2366: \>\>\>$\{k:0\leq k<\S curSize/\land \S val/(\T Y/[k])\neq \B null/\}])$\\

2367: \>\>$f~ \T is injective/$, \\

2368: \>where $h=\T H/(\T next/(\T currInd/))$

2369: \end{tab1}

2370: 

2371: 

2372: \medbreak Invariants concerning procedure \S find/ (5\dots 14)

2373: \begin{tab1} 

2374: 

2375: %\\ ! G-a-a!\\

2376: \S fi1:/ \>$a_{\it fi}\neq \B 0/$ \\

2377: 

2378: %\\ ! G-n-find1!\\

2379: \S fi2:/ \>$ pc\in \{6,11\}~\implies \quad n_{\it fi}=0$ \\

2380: 

2381: 

2382: %\\ ! G-find4!\\

2383: \S fi3:/ \>$ pc \in \{7,8,13\} ~\implies \quad l_{\it fi}=h_{\it fi}.\T size/$ \\

2384: 

2385: %\\ ! G-find5!\\

2386: \S fi4:/ \>$ pc \in [6,13]\Land pc\neq 10~\implies \quad h_{\it fi}=\T H/(\S index/)$ \\

2387: 

2388: 

2389: %\\ ! G-n-size-a!\\

2390: \S fi5:/ \>$ pc=7 \Land h_{\it fi}=\T H/(\T currInd/)~\implies \quad 

2391: n_{\it fi} < \S curSize/$ \\

2392: 

2393: %\\ ! G-r-find2!\\

2394: \S fi6:/ \>$ pc=8\Land h_{\it fi}=\T H/(\T currInd/)\Land\neg \S Find/(r_{\it fi},a_{\it fi})

2395: \Land r_{\it fi}\neq\B done/$\\

2396: \>$\implies\ \neg\ \S Find/(\T Y/[\S key/(a_{\it fi},\S curSize/,n_{\it fi})],

2397: a_{\it fi})$ \\

2398: 

2399: %\\ ! G-r-find1!\\

2400: \S fi7:/ \>$ pc=13 \Land h_{\it fi}=\T H/(\T currInd/)\Land \neg\S Find/(r_{\it fi},a_{\it fi})

2401: \Land m < n_{\it fi}$ \\

2402: \> $ \implies\quad \neg\S Find/(\T Y/[\S key/(a_{\it fi},\S curSize/,m)], a_{\it fi})$ \\

2403: 

2404: %\\ ! G-find3!\\

2405: \S fi8:/ \>$ pc\in \{7,8\}\Land h_{\it fi}=\T H/(\T currInd/) \Land m < n_{\it fi}$\\

2406: \> $ \implies\quad

2407: \neg \S Find/(\T Y/[\S key/(a_{\it fi},\S curSize/,m)],a_{\it fi})$ \\

2408: 

2409: %\\ !  G-find2!\\

2410: \S fi9:/ \>$ $\=$pc=7\Land\S Find/(t,a_{\it fi})~\implies \quad \T X/(a_{\it fi})=\S val/(t)$, \\

2411: \>where $t=h_{\it fi}.\T table/[\S key/(a_{\it fi},l_{\it fi},n_{\it fi})]$\\

2412: 

2413: %\\ !  G-find1!\\

2414: \S fi10:/ \>$  pc \notin (1,7] \Land \S Find/(r_{\it fi},a_{\it fi})~\implies \quad

2415: \S val/(r_{\it fi})=rS_{\it fi} $ \\

2416: 

2417: %\\ ! G-old-a!\\

2418: \S fi11:/ \>$pc=8\Land \S oldp/(r_{\it fi})\Land \S index/=\T currInd/$\\

2419: \>$\implies\ \T next/(\T currInd/)\neq 0$ 

2420: \end{tab1}

2421: 

2422: 

2423: \medbreak Invariants concerning procedure \S delete/ (15\dots 26)

2424: \begin{tab1} 

2425: 

2426: %\\ ! G-a-b!\\

2427: \S de1:/ \>$a_{\it del}\neq \B 0/$ \\

2428: 

2429: %\\ ! G-delete4!\\

2430: \S de2:/ \>$ pc \in\{17,18\}~\implies \quad l_{\it del}=h_{\it del}.\T size/$ \\

2431: 

2432: %\\ ! G-delete5!\\

2433: \S de3:/ \>$ pc\in [16,25] \Land pc\neq 20~\implies \quad h_{\it del}=\T H/(\S index/)$ \\

2434: 

2435: %\\ ! G-find7-a!\\

2436: \S de4:/ \>$ pc=18~\implies \quad k_{\it del}=\S key/(a_{\it del},l_{\it del},n_{\it del})$ \\

2437: 

2438: %\\ ! G-s-delete1!\\

2439: \S de5:/ \>$ pc\in \{16,17\} \Lor \S Deleting/ ~\implies \quad \neg suc_{\it del}$\\

2440: 

2441: %\\ ! G-s-delete2!\\

2442: \S de6:/ \> $ \S Deleting/ \Land sucS_{\it del}~\implies \quad r_{\it del}\neq \B null/$ \\

2443: 

2444: %\\ ! G-find6-a!\\

2445: \S de7:/ \>$ pc=18\Land \neg\ \S oldp/(h_{\it del}.\T table/[k_{\it del}])~\implies \quad 

2446: h_{\it del}=\T H/(\T currInd/)$ \\

2447: 

2448: %\\ !  G-n-size-b!\\

2449: \S de8:/ \>$ pc \in \{17,18\} \Land h_{\it del}=\T H/(\T currInd/)~\implies \quad

2450:  n_{\it del}<\S curSize/$\\

2451: 

2452: %\\ ! G-r-delete1!\\

2453: \S de9:/ \>$pc=18\Land h_{\it del}=\T H/(\T currInd/)$\\

2454: \>$\land~ (\S val/(r_{\it del})\neq\B null/\Lor r_{\it del}=\B del/)$\\

2455: \>$\implies\ r\neq \B null/\Land (r=\B del/\Lor 

2456: \S ADR/(r)=\S ADR/(r_{\it del}))$,\\

2457: \>where $r=\T Y/[\S key/(a_{\it del},h_{\it del}.size,n_{\it del})]$\\

2458: 

2459: %\\ ! G-delete3!\\

2460: \S de10:/ \>$ pc\in\{17,18\}\Land h_{\it del}=\T H/(\T currInd/) \Land m < n_{\it del}) $\\

2461: \> $ \implies\quad \neg \S Find/(\T Y/[\S key/(a_{\it del},\S curSize/,m)],a_{\it del})$\\

2462: 

2463: %\\ ! G-delete2!\\\

2464: \S de11:/ \>$ pc\in \{17,18\} \Land \S Find/(t,a_{\it del})~\implies \quad 

2465: \T X/(a_{\it del})=\S val/(t)$,\\

2466: \>where $t=h_{\it del}.\T table/[\S key/(a_{\it del},l_{\it del},n_{\it del})]$\\

2467: 

2468: %\\ ! G-old-b!\\

2469: \S de12:/ \>$pc=18\Land \S oldp/(r_{\it del})\Land \S index/=\T currInd/$\\

2470: \>$\implies\ \T next/(\T currInd/)\neq 0$ \\

2471: 

2472: %\\ ! G-find6-1-a!\\

2473: \S de13:/ \>$ pc=18~\implies \quad k_{\it del}<\T H/(\S index/).\T size/$ \\

2474: %\>;\qquad ELIMINATED by (fi7-a),(del4),(del5) and axiom (KEYinRange).

2475: \end{tab1}

2476: 

2477: \medbreak\noindent

2478: where $Deleting$ is characterized by

2479: \begin{tab1}

2480: \+ $\S Deleting/\EQ $\\

2481: $pc\in [18,21]\Lor pc\in [59,65]\Land return_{\it gA}=20$\\

2482: $\lor~ pc\in [67,72]\Land ($\=$return_{\it rA}=59 \land 

2483: return_{\it gA}=20$\\

2484: \>$\lor~ return_{\it rA}=90 \land return_{\it ref}=20)$\\

2485: $\lor\ pc\geq 90 \Land  return_{\it ref}=20$

2486: \end{tab1}

2487: 

2488: \medbreak Invariants concerning procedure \S insert/ (27\dots 52)

2489: 

2490: \begin{tab1}

2491: %\\ ! G-a-c!\\

2492: \S in1:/ \>$a_{\it ins}=\S ADR/(v_{\it ins})\Land v_{\it ins}\neq \B null/$ \\

2493: 

2494: %\\ ! G-insert4!\\

2495: \S in2:/ \>$pc\in [32,35]~\implies \quad l_{\it ins}=h_{\it ins}.\T size/$ \\

2496: 

2497: %\\ ! G-insert5!\\

2498: \S in3:/ \>$pc\in [28,41]\Land pc\notin \{30,36\}~\implies \quad h_{\it ins}=\T H/(\S index/)$ \\

2499: 

2500: %\\ ! G-find7-b!\\

2501: \S in4:/ \>$ pc\in \{33,35\}~\implies \quad 

2502: k_{\it ins}=\S key/(a_{\it ins},l_{\it ins},n_{\it ins})$ \\

2503: 

2504: %\\ ! G-s-insert1!\\

2505: \S in5:/ \>$pc\in [32,33]\Lor \S Inserting/ ~\implies \quad \neg suc_{\it ins}$\\

2506: 

2507: %\\ ! G-s-insert2!\\

2508: \S in6:/ \> $\S Inserting/\Land sucS_{\it ins}~\implies \quad

2509: \S ADR/(r_{\it ins})\neq a_{\it ins}$\\

2510: 

2511: %\\ ! G-find6-b!\\

2512: \S in7:/ \>$ pc=35\Land \neg\ \S oldp/(h_{\it ins}.\T table/[k_{\it ins}])~\implies \quad 

2513: h_{\it ins}=\T H/(\T currInd/)$ \\

2514: 

2515: %\\ ! G-n-size-c!\\

2516: \S in8:/ \>$ pc \in \{33,35\} \Land h_{\it ins}=\T H/(\T currInd/)~\implies \quad n_{\it ins}<\S curSize/$\\

2517: 

2518: %\\ ! G-r-insert1!\\

2519: \S in9:/ \>$pc=35\Land h_{\it ins}=\T H/(\T currInd/)$\\

2520: \>$\land~ (\S val/(r_{\it ins})\neq\B null/\Lor r_{\it ins}=\B del/)$\\

2521: \>$\implies\ r\neq \B null/\Land (r=\B del/\Lor \S ADR/(r)=\S ADR/(r_{\it ins}))$,\\

2522: \>where $r=\T Y/[\S key/(a_{\it ins},h_{\it ins}.size,n_{\it ins})]$\\

2523: 

2524: %\\ ! G-insert3!\\

2525: \S in10:/ \>$pc\in \{32,33,35\}\Land h_{\it ins}=\T H/(\T currInd/) \Land m < n_{\it ins} $\\

2526: \>$ \implies\quad \neg \S Find/(\T Y/[\S key/(a_{\it ins},\S curSize/,m)],a_{\it ins})$\\

2527: 

2528: %\\ ! G-insert2!\\

2529: \S in11:/ \>$pc\in \{ 33,35\}\Land \S Find/(t,a_{\it ins})~\implies \quad\ \T X/(a_{\it ins})=\S val/(t)$,\\

2530: \>where $t=h_{\it ins}.\T table/[\S key/(a_{\it ins},l_{\it ins},n_{\it ins})]$ \\

2531: 

2532: %\\ ! G-old-c!\\

2533: \S in12:/ \>$pc=35\Land \S oldp/(r_{\it ins})\Land \S index/=\T currInd/$\\

2534: \>$\implies\ \T next/(\T currInd/)\neq 0$ \\

2535: 

2536: %\\ ! G-find6-1-b!\\

2537: \S in13:/ \>$ pc=35~\implies \quad k_{\it ins}<\T H/(\S index/).\T size/$ \\

2538: %\>;\qquad ELIMINATED by (fi7-b),(in4),(in5) and axiom (KEYinRange).

2539: \end{tab1}

2540: where $Inserting$ is characterized by

2541: \begin{tab1}

2542: \+ $\S Inserting/ \EQ $\\

2543: $pc\in [35,37]\Lor pc\in [59,65]\Land return_{\it gA}=36$\\

2544: $\lor~ pc\in [67,72]\Land ($\=$return_{\it rA}=59 \land 

2545: return_{\it gA}=36$\\

2546: \>$\lor~ return_{\it rA}=90 \land return_{\it ref}=36)$\\

2547: $\lor~ pc\geq 90 \Land  return_{\it ref}=36$

2548: \end{tab1}

2549: 

2550: 

2551: \medbreak Invariants concerning procedure \S assign/ (43\dots 57)

2552: 

2553: \begin{tab1}

2554: %\\ ! G-a-d!\\

2555: \S as1:/ \>$ a_{\it ass}=\S ADR/(v_{\it ass})\Land v_{\it ass}\neq \B null/$ \\

2556: 

2557: %\\ ! G-assign4!\\

2558: \S as2:/ \>$pc\in [48,50]~\implies \quad l_{\it ass}=h_{\it ass}.\T size/$ \\

2559: 

2560: %\\ ! G-assign5!\\

2561: \S as3:/ \>$pc\in [44,57]\Land pc\notin \{46,51\}~\implies \quad h_{\it ass}=\T H/(\S index/)$ \\

2562: 

2563: %\\ ! G-find7-c!\\

2564: \S as4:/ \>$ pc\in \{49,50\}~\implies \quad 

2565: k_{\it ass}=\S key/(a_{\it ass},l_{\it ass},n_{\it ass})$\\

2566: 

2567: %\\ ! G-find6-c!\\

2568: \S as5:/ \>$ pc=50\Land \neg\ \S oldp/(h_{\it ass}.\T table/[k_{\it ass}])~\implies \quad h_{\it ass}=\T H/(\T currInd/)$\\

2569: 

2570: %\\ ! G-n-size-d!\\

2571: \S as6:/ \>$ pc = 50 \Land h_{\it ass}=\T H/(\T currInd/)~\implies \quad n_{\it ass}<\S curSize/$ \\

2572: 

2573: %\\ ! G-r-assign1!\\

2574: \S as7:/ \>$pc=50\Land h_{\it ass}=\T H/(\T currInd/)$\\

2575: \>$\land~ (\S val/(r_{\it ass})\neq\B null/\Lor r_{\it ass}=\B del/)$\\

2576: \>$\implies\ r\neq \B null/\Land (r=\B del/\Lor \S ADR/(r)=\S ADR/(r_{\it ass}))$,\\

2577: \>where $r=\T Y/[\S key/(a_{\it ass},h_{\it ass}.size,n_{\it ass})]$ \\

2578: 

2579: %\\ ! G-assign3!\\

2580: \S as8:/ \>$pc\in \{48,49,50\}\Land h_{\it ass}=\T H/(\T currInd/) \Land m < n_{\it ass} $\\

2581: \> $ \implies\quad \neg \S Find/(\T Y/[\S key/(a_{\it ass},\S curSize/,m)],a_{\it ass})$\\

2582: 

2583: %\\ ! G-assign2!\\

2584: \S as9:/ \>$pc=50 \Land \S Find/(t,a_{\it ass})~\implies \quad \T X/(a_{\it ass})=\S val/(t)$,\\

2585: \>where $t=h_{\it ass}.\T table/[\S key/(a_{\it ass},l_{\it ass},n_{\it ass})]$\\

2586: 

2587: %\\ ! G-old-d!\\

2588: \S as10:/ \>$pc=50\Land \S oldp/(r_{\it ass}sign)\Land \S index/=\T currInd/$\\

2589: \>$\implies\ \T next/(\T currInd/)\neq 0$ \\

2590: 

2591: %\\ ! G-find6-1-c!\\

2592: \S as11:/ \>$ pc=50~\implies \quad k_{\it ass}<\T H/(\S index/).\T size/$ \\

2593: %\>;\qquad ELIMINATED by (fi7-c),(as4),(as5) and axiom (KEYinRange).

2594: \end{tab1}

2595: 

2596: 

2597: \medbreak Invariants concerning procedure \S releaseAccess/ (67\dots 72)

2598: 

2599: \begin{tab1}

2600: 

2601: %\\ ! G-H-index2!\\

2602: \S rA1:/ \>$ h_{\it rA}<\T H/_-\T index/$\\

2603: 

2604: %\\ ! G-H6!\\

2605: \S rA2:/ \>$ pc\in [70,71]~\implies \quad h_{\it rA}\neq 0$ \\

2606: 

2607: %\\ ! G-releaseAccess6!\\

2608: \S rA3:/ \>$pc=71 ~\implies \quad \T Heap/(h_{\it rA})\neq\bot$ \\

2609: 

2610: %\\ ! G-H3!\\

2611: \S rA4:/ \>$ pc=71~\implies \quad \T H/(i_{\it rA})=0$ \\

2612: 

2613: %\\ ! G-H7!\\

2614: \S rA5:/ \>$ pc=71~\implies \quad h_{\it rA}\ne\T H/(i)$ \\

2615: 

2616: %\\ ! G-releaseAccess1-a!\\

2617: \S rA6:/ \>$pc=70~\implies \quad\T H/(i_{\it rA})\neq\T H/(\T currInd/)$ \\

2618: 

2619: %\\ ! G-releaseAccess1-b!\\

2620: \S rA7:/ \>$pc=70$\\

2621: \>$\land\ (pc.r \in [1,58]\Lor pc.r>65\land 

2622: \neg (pc.r \in [67,72]\land i_{\it rA}.r=\S index/.r))$\\

2623: \>$\implies\ \T H/(i_{\it rA})\neq \T H/(\S index/.r)$\\

2624: 

2625: %\\ ! G-i-releaseAccess1!\\

2626: \S rA8:/ \>$pc=70~\implies \quad i_{\it rA}\neq\T next/(\T currInd/)$ \\

2627: 

2628: %\\ ! G-releaseAccess2!\\

2629: \S rA9:/ \>$pc\in [68,72]\land\ (h_{\it rA}=0\Lor h_{\it rA}\neq \T H/(i_{\it rA}))$\\

2630: \> $\implies\ \T H/(i_{\it rA})=0$ \\

2631: 

2632: %\\ ! G-i-releaseAccess2!\\

2633: \S rA10:/ \>$pc\in [67,72]\Land return_{\it rA}\in \{0,59\}~\implies\ i_{\it rA}=\S index/$\\

2634: 

2635: %\\ ! G-releaseAccess3!\\

2636: \S rA11:/ \>$pc\in [67,72]\Land return_{\it rA}\in \{77,90\}~\implies\ i_{\it rA}\neq \S index/$ \\

2637: 

2638: %\\ ! G-releaseAccess5!\\

2639: \S rA12:/ \>$pc\in [67,72]\Land return_{\it rA}=77~\implies \quad\T next/(\S index/)\neq 0$ \\

2640: 

2641: 

2642: %\\ ! G-releaseAccess8!\\

2643: \S rA13:/ \>$pc=71 \Land pc.r=71 \Land p\neq r ~\implies \quad h_{\it rA}\neq h_{\it rA}.r$ \\

2644: 

2645: %\\ ! G-i-releaseAccess3!\\

2646: \S rA14:/ \>$pc=71 \Land pc.r=71 \Land p\neq r ~\implies \quad i_{\it rA}\neq i_{\it rA}.r$

2647: \end{tab1}

2648: 

2649: 

2650: \medbreak Invariants concerning procedure \S newTable/ (77\dots 84)

2651: 

2652: \begin{tab1}

2653: 

2654: %\\ ! G-newTable9!\\

2655: \S nT1:/ \>$  pc \in [81,82] ~\implies \quad \T Heap/(\T H/(i_{\it nT}))=\bot$ \\

2656: 

2657: %\\ ! G-newTable2!\\

2658: \S nT2:/ \>$ pc \in [83,84]~\implies \quad \T Heap/(\T H/(i_{\it nT}))\neq \bot$ \\

2659: 

2660: 

2661: %\\ ! G-next-i-newTable!\\

2662: \S nT3:/ \>$ pc=84 ~\implies \quad\T next/(i_{\it nT})=0$ \\

2663: 

2664: %\\ ! G-newTable4!\\

2665: \S nT4:/ \>$ pc \in [83,84] ~\implies \quad \T H/(i_{\it nT}).\T dels/=0$ \\

2666: 

2667: %\\ ! G-newTable6!\\

2668: \S nT5:/ \>$  pc \in [83,84] ~\implies \quad \T H/(i_{\it nT}).\T occ/=0$ \\

2669: 

2670: %\\ ! G-newTable7!\\

2671: \S nT6:/ \>$  pc \in [83,84] ~\implies \quad 

2672: \T H/(i_{\it nT}).\T bound/+2*P< \T H/(i_{\it nT}).\T size/$ \\

2673: 

2674: %\\ ! G-newTable8!\\

2675: \S nT7:/ \>$  pc \in [83,84] \Land \S index/=\T currInd/$\\

2676: \>$\implies \quad \T H/(\T currInd/).\T bound/-\T H/(\T currInd/).\T dels/+2*P< \T H/(i_{\it nT}).\T bound/$ \\

2677: 

2678: %\\ ! G-newTable5!\\

2679: \S nT8:/ \>$ pc \in [83,84]\Land k < \T H/(i_{\it nT}).\T size/

2680: ~\implies \quad \T H/(i_{\it nT}).\T table/[k]=\B null/$ \\

2681: 

2682: %\\ ! G-i-newTable-a!\\

2683: \S nT9:/ \>$ pc \in [81,84]~\implies \quad i_{\it nT}\neq \T currInd/$ \\

2684: 

2685: %\\ ! G-i-newTable-b!\\

2686: \S nT10:/ \>$ pc \in [81,84]\Land (pc.r\in [1,58]\Lor pc.r\geq 62 \Land pc.r\neq 65) $\\

2687: \>$\implies\quad i_{\it nT}\ne \S index/.r$\\

2688: 

2689: %\\ ! G-i-newTable4!\\

2690: \S nT11:/ \>$ pc\in [81,84]~\implies \quad i_{\it nT}\neq \T next/(\T currInd/)$\\

2691: 

2692: %\\ ! G-newTable1-a!\\

2693: \S nT12:/ \>$ pc \in [81,84]~\implies \quad\T H/(i_{\it nT})\neq \T H/(\T currInd/)$\\

2694: %\>;\qquad ELIMINATED by (i-nT-a),(k0-a),(h1).

2695: 

2696: %\\ ! G-newTable1-b!\\

2697: \S nT13:/ \>$ pc \in [81,84]$\\

2698: \>$\land\ (pc.r \in [1,58]\Lor pc.r>65\land \neg (pc.r \in [67,72]\land i_{\it rA}.r=\S index/.r))$\\

2699: \>$\implies\quad \T H/(i_{\it nT})\ne \T H/(\S index/.r)$ \\

2700: 

2701: %\\ ! G-i-newTable2!\\

2702: \S nT14:/ \>$ pc\in [81,84]\Land pc.r\in [67,72]~\implies \quad 

2703: i_{\it nT}\ne i_{\it rA}.r$\\

2704: 

2705: %\\ ! G-newTable3!\\

2706: \S nT15:/ \>$ pc \in [83,84]\Land pc.r\in [67,72]~\implies \quad 

2707: \T H/(i_{\it nT})\ne \T H/(i_{\it rA}.r)$ \\

2708: 

2709: %\\ ! G-i-newTable3!\\

2710: \S nT16:/ \>$ pc\in [81,84]\Land pc.r\in [81,84]\Land p \ne r

2711: ~\implies \quad i_{\it nT}\ne i_{\it nT}.r$ \\

2712: 

2713: %\\ ! G-i-newTable5!\\

2714: \S nT17:/ \>$ pc\in [81,84]\Land pc.r \in [95,99]\Land \S index/.r=\T currInd/$\\

2715: \> $\implies\quad i_{\it nT}\ne i_{\it mig}.r$\\

2716: 

2717: %\\ ! G-i-newTable1!\\

2718: \S nT18:/ \>$ pc\in [81,84]\Land pc.r\geq 99~\implies \quad  i_{\it nT}\ne i_{\it mig}.r$

2719: \end{tab1}

2720: 

2721: 

2722: \medbreak Invariants concerning procedure \S migrate/ (94\dots 105)

2723: 

2724: \begin{tab1}

2725: 

2726: %\\ ! G-migrate8,G-index1 !\\

2727: \S mi1:/ \>$ pc=98 \Lor pc\in \{104,105\} ~\implies \quad \S index/\neq \T currInd/$\\

2728: 

2729:  %\\ ! G-i-migrate1!\\

2730: \S mi2:/ \>$ pc\geq 95~\implies \quad i_{\it mig}\neq \S index/$ \\

2731: 

2732: %\\ ! G-i-migrate6!\\

2733: \S mi3:/ \>$ pc=94~\implies \quad \T next/(\S index/)>0$\\

2734: 

2735: %\\ ! G-i-migrate4!\\

2736: \S mi4:/ \>$ pc\geq 95~\implies \quad i_{\it mig}\neq 0$\\

2737: 

2738: %\\ ! G-i-migrate3!\\

2739: \S mi5:/ \>$ pc \geq 95~\implies \quad i_{\it mig}=\T next/(\S index/)$ \\

2740: 

2741:  %\\ ! G-i-migrate2, G-i-migrate7!\\

2742: \S mi6:/ \>$ pc.r=70$\\

2743: \>$\land~ (pc\in [95,102) \Land \S index/=\T currInd/ \Lor pc \in [102,103] \Lor pc\geq 110)$\\

2744: \>$\implies \quad i_{\it rA}.r\neq i_{\it mig}$ \\

2745: 

2746: %\\ ! G-next-i-migrate,G-next-i-migrate1!\\

2747: \S mi7:/ \>$ pc \in [95,97]\Land \S index/=\T currInd/\Lor pc\geq 99$\\

2748: \>$\implies \quad i_{\it mig}\neq \T next/(i_{\it mig})$\\

2749: 

2750: %\\ ! G-next-i-migrate2!\\

2751: \S mi8:/ \>$ (pc \in [95,97]\Lor pc \in [99,103] \Lor pc\geq 110)\Land \S index/=\T currInd/$\\

2752: \>$\implies \quad \T next/(i_{\it mig})=0$\\

2753: 

2754:  %\\ !  G-i-migrate-a !\\

2755: \S mi9:/ \>$(pc \in [95,103]\Lor pc\geq 110)\Land \S index/=\T currInd/$ \\

2756: \>\>$\implies \quad \T H/(i_{\it mig})\neq \T H/(\T currInd/)$\\

2757: 

2758:  %\\ !  G-i-migrate-b !\\

2759: \S mi10:/ \>$(pc \in [95,103]\Lor pc\geq 110)\Land \S index/=\T currInd/ $ \\

2760: \> $ \land\;\; (pc.r \in [1,58]\Lor pc.r\geq 62\Land pc.r\neq 65)$\\

2761: \>$\implies\quad \T H/(i_{\it mig}) \neq \T H/(\S index/.r) $ \\

2762: 

2763: %\\ ! G-moveContents9-1!\\

2764: \S mi11:/ \>$ pc=101 \Land \S index/=\T currInd/ \Lor pc=102$\\

2765: \>$\implies \quad h_{\it mig}=\T H/(i_{\it mig})$\\

2766: 

2767: %\\ ! G-migrate2,G-migrate2-1!\\

2768: \S mi12:/ \>$pc\geq 95\Land \S index/=\T currInd/ \Lor pc\in \{102,103\}\Lor pc\geq 110$\\

2769: \>$\implies \quad\ \T Heap/(\T H/(i_{\it mig}))\neq \bot$ \\

2770: 

2771:  %\\ ! G-migrate1!\\

2772: \S mi13:/ \>$pc=103\Land \S index/=\T currInd/\Land k < \S curSize/~$\\

2773: \>$\implies \quad \T H/(\S index/).\T table/[k]=\B done/$\\

2774: 

2775:  %\\ ! G-migrate3-a!\\

2776: \S mi14:/ \>$$\=$pc=103\Land \S index/=\T currInd/\Land n < \T H/(i_{\it mig}).\T size/$\\

2777: \>\>$\land\quad \S LeastFind/(\T H/(i_{\it mig}),a,n)$\\

2778: \>\>$\implies\quad \T X/(a)=\S val/(\T H/(i_{\it mig})[\S key/(a,\T H/(i_{\it mig}).\T size/,n)])$ \\

2779: 

2780:  %\\ ! G-migrate3-b!\\

2781: \S mi15:/ \>$$\=$pc=103\Land \S index/=\T currInd/\Land n < \T H/(i_{\it mig}).\T size/$\\

2782: \>\>$\land\quad \T X/(a)=

2783: \S val/(\T H/(i_{\it mig}).\T table/[\S key/(a,\T H/(i_{\it mig}).\T size/,n)]

2784: \neq\B null/$\\

2785: \>\>$\implies\quad \S LeastFind/(\T H/(i_{\it mig}),a,n)$ \\

2786: 

2787:  %\\ ! G-migrate4\\!\\

2788: \S mi16:/ \>$pc=103\Land \S index/=\T currInd/\Land k < \T H/(i_{\it mig}).\T size/$\\

2789: \>$ \implies\quad \neg \S oldp/(\T H/(i_{\it mig}).\T table/[k])$\\

2790: 

2791:  %\\ !  G-migrate5-a!\\

2792: \S mi17:/ \>$pc=103\Land \S index/=\T currInd/ \Land \T X/(a)\neq \B null/\Land 

2793: k < h.\T size/$\\

2794: \> $ \land\;\; \T X/(a)=\S val/(h.\T table/[\S key/(a,h.\T size/,k)])

2795: \Land k \ne n < h.\T size/$\\

2796: \> $\implies\quad \S ADR/(h.\T table/.[\S key/(a,h.\T size/,n)])\ne a $,\\

2797: \>where $ h=\T H/(i_{\it mig})$ \\

2798: 

2799: %\\ !  G-migrate5-b!\\

2800: \S mi18:/ \>$pc=103\Land \S index/=\T currInd/ \Land \T X/(a)=\B null/\Land k < h.\T size/$\\

2801: \>$ \implies\quad \S val/(h.\T table/[\S key/(a,h.\T size/,k)]) = \B null/$\\

2802: \>\>$\Lor~ \S ADR/(h.\T table/[\S key/(a,h.\T size/,k)])\ne a $, \\

2803: \>where $ h=\T H/(i_{\it mig})$\\

2804: 

2805: %\\ ! G-migrate6!\\

2806: \S mi19:/ \>$ pc=103\Land \S index/=\T currInd/\Land \T X/(a)\neq \B null /$\\

2807: \> $ \implies\quad \exists m < h.\T size/: 

2808: \T X/(a)=\S val/(h.\T table/[\S key/(a,h.\T size/,m)]$, \\

2809: \>where $h=\T H/(i_{\it mig})$\\

2810: 

2811:  %\\ ! G-migrate6-3!\\

2812: \S mi20:/ \>$ $\=$pc=117 \Land \T X/(a)\neq \B null/

2813: \Land \S val/(\T H/(\S index/).\T table/[i_{\it mC}])\neq \B null/$\\

2814: \>$\lor~ pc\geq 126\Land \T X/(a)\neq \B null/\Land \S index/=\T currInd/$\\

2815: \>$\lor~ pc=125 \Land \T X/(a)\neq \B null/\Land \S index/=\T currInd/$\\

2816: \>\>$ \Land $\=$(b_{\it mE} \Lor \S val/(w_{\it mE})\neq \B null/$\\

2817: \>\>\>$\Land a_{\it mE}=\S ADR/(w_{\it mE}))$ \\

2818: \>$\implies\ \exists m < h.\T size/: 

2819: \T X/(a)=\S val/(h.\T table/[\S key/(a,h.\T size/,m)])$,\\

2820: \>where $a=\S ADR/(\T Y/[i_{\it mC}])$ and $h=\T H/(\T next/(\T currInd/))$

2821: \end{tab1}

2822: 

2823: 

2824: \medbreak Invariants concerning procedure \S moveContents/ (110\dots 118):

2825: \begin{tab1}

2826: 

2827: %\\ ! G-moveContents9!\\

2828: \S mC1:/ \>$ pc=103 \Lor pc \geq 110~\implies \quad to=\T H/(i_{\it mig})$\\

2829: 

2830: %\\ ! G-moveContents1!\\

2831: \S mC2:/ \>$ pc\geq 110~\implies \quad from=\T H/(\S index/)$\\

2832: 

2833: %\\ ! G-moveContents11!\\

2834: \S mC3:/ \>$ pc>102\Land m \in toBeMoved~\implies \quad m<\T H/(\S index/).\T size/$\\

2835: 

2836: 

2837: %\\ ! G-moveContents10!\\

2838: \S mC4:/ \>$ pc=111~\implies \quad \exists m < from.\T size/:m\in toBeMoved$ \\

2839: 

2840: %\\ ! G-moveContents2!\\

2841: \S mC5:/ \>$ pc\geq 114\Land pc\neq 118~\implies \quad v_{\it mC}\neq\B done/$ \\

2842: 

2843: %\\ ! G-moveContents3!\\

2844: \S mC6:/ \>$ pc\geq 114~\implies \quad i_{\it mC}<\T H/(\S index/).\T size/$ \\

2845: 

2846: 

2847: %\\ ! G-moveContents4 !\\

2848: \S mC7:/ \>$ pc=118~\implies \quad \T H/(\S index/).\T table/[i_{\it mC}]=\B done/$ \\

2849: 

2850: %\\ ! G-moveContents5!\\

2851: \S mC8:/ \>$pc\geq 110 \Land k < \T H/(\S index/).\T size/\Land 

2852: k\notin toBeMoved$\\

2853: \>$\implies \quad \T H/(\S index/).\T table/ [k]=\B done/$\\

2854: 

2855: %\\ ! G-migrate7!\\

2856: \S mC9:/ \>$ pc \geq 110\Land \S index/=\T currInd/\Land toBeMoved=\emptyset $\\

2857: \>$\land\;\; k < \T H/(\S index/).\T size/$\\

2858: \> $\implies \quad \T H/(\S index/).\T table/[k]=\B done/$ \\

2859: 

2860: %\\ ! G-moveContents6 \\!\\

2861: \S mC10:/ \>$ pc\geq 116\Land \S val/(v_{\it mC})\neq\B null/$\\

2862: \>$\land~ \T H/(\S index/).\T table/[i_{\it mC}]=\B done/$ \\

2863: \>$\implies \quad \T H/(i_{\it mig}).\T table/[\S key/(a,\T H/(i_{\it mig}).\T size/,0)]\neq \B null/$, \\

2864: \>where $a=\S ADR/(v_{\it mC})$ \\

2865: 

2866: 

2867: %\\ ! G-moveContents7!\\

2868: \S mC11:/ \>$ pc\geq 116 \Land\T H/(\S index/).\T table/[i_{\it mC}]\neq \B done/$ \\

2869: \>$\implies\quad \S val/(v_{\it mC})=\S val/(\T H/(\S index/).\T table/[i_{\it mC}])$\\

2870: \>$\Land~ \S oldp/(\T H/(\S index/).\T table/[i_{\it mC}])$\\

2871: 

2872: 

2873: %\\ ! G-moveContents7-1!\\

2874: \S mC12:/ \>$ pc\geq 116\Land \S index/=\T currInd/\Land\S val/(v_{\it mC})\neq\B null/$ \\

2875: \>$\implies \quad \S val/(v_{\it mC})=\S val/(\T Y/[i_{\it mC}])$ 

2876: \end{tab1}

2877: 

2878: 

2879: \medbreak Invariants concerning procedure \S moveElement/ (120\dots 126):

2880: 

2881: \begin{tab1} 

2882: %\\ ! G-moveContents8!\\

2883: \S mE1:/ \>$ pc\geq 120~\implies \quad \S val/(v_{\it mC})=v_{\it mE}$ \\

2884: 

2885: %\\ ! G-moveElement1!\\

2886: \S mE2:/ \>$ pc \geq 120 ~\implies \quad v_{\it mE}\neq \B null/$\\

2887: 

2888: %\\ ! G-moveElement2!\\

2889: \S mE3:/ \>$ pc \geq 120 ~\implies \quad to=\T H/(i_{\it mig})$\\

2890: 

2891: %\\ ! G-moveElement11!\\

2892: \S mE4:/ \>$ pc \geq 121~\implies \quad a_{\it mE}=\S ADR/(v_{\it mC})$\\

2893: 

2894: %\\ ! G-moveElement14!\\

2895: \S mE5:/ \>$ pc\geq 121~\implies \quad m_{\it mE}=to.\T size/$\\

2896: 

2897: %\\ ! G-moveElement12!\\

2898: \S mE6:/ \>$ pc\in \{121,123\}~\implies \quad \neg b_{\it mE}$\\

2899: 

2900: %\\ ! G-moveElement7!\\

2901: \S mE7:/ \>$ pc=123 ~\implies \quad k_{\it mE}=\S key/(a_{\it mE},to.\T size/,n_{\it mE})$\\

2902: 

2903: %\\ ! G-moveElement13!\\

2904: \S mE8:/ \>$ pc\geq 123~\implies \quad k_{\it mE}<\T H/(i_{\it mig}).\T size/$\\

2905: 

2906: %\\ ! G-moveElement6!\\

2907: \S mE9:/ \>$ pc=120 $\\

2908: \>$\land~ to.\T table/[\S key/(\S ADR/(v_{\it mE}),to.\T size/,0)]=\B null/$\\

2909: \>$\implies \quad \S index/=\T currInd/$\\

2910: 

2911: %\\ ! G-moveElement3!\\

2912: \S mE10:/ \>$ pc \in \{121,123\}$\\

2913: \>$\land~ to.\T table/[\S key/(a_{\it mE},to.\T size/,n_{\it mE})]=\B null/$\\

2914: \>$\implies \quad \S index/=\T currInd/$\\

2915: 

2916:  %\\ !  G-moveElement4!\\

2917: \S mE11:/ \>$ pc \in \{121,123\}\Land pc.r=103 $\\

2918: \>$\land~ to.\T table/[\S key/(a_{\it mE},to.\T size/,n_{\it mE})]=\B null/$\\

2919: \>$\implies\quad \S index/.r\ne \T currInd/$\\

2920: 

2921: %\\ ! G-moveElement8\\!\\

2922: \S mE12:/ \>$pc\in \{121,123\}\Land \T next/(\T currInd/)\neq 0 \Land to=\T H/(\T next/(\T currInd/))$\\

2923: \>$\implies \quad n_{\it mE}<\T H/(\T next/(\T currInd/)).\T size/$ \\

2924: 

2925: 

2926: %\\ ! G-moveElement10-1!\\

2927: \S mE13:/ \>$ pc \in \{123,125\}\Land w_{\it mE}\neq\B null/$\\

2928: \>$\implies\quad \S ADR/(w_{\it mE})=\S ADR/(to.\T table/[k_{\it mE}])$\\

2929: \>$~\Lor~ to.\T table/[k_{\it mE}]\in \{\B del/,\B done/\}$\\

2930: 

2931: %\\ ! G-moveElement10!\\

2932: \S mE14:/ \>$ pc \geq 123 \Land w_{\it mE}\neq\B null/$\\

2933: \>$\implies \quad \T H/(i_{\it mig}).\T table/[k_{\it mE}]\neq\B null/$\\

2934: 

2935: %\\ ! G-moveElement9!\\

2936: \S mE15:/ \>$ pc=117 \Land \S val/(v_{\it mC})\neq \B null/$\\

2937: \>$\lor~ pc\in \{121,123\}\Land n_{\it mE}>0$\\

2938: \>$\lor~ pc=125$\\

2939: \>$\implies \quad h.\T table/[\S key/(\S ADR/(v_{\it mC}),h.\T size/,0)]

2940: \neq\B null/$,\\

2941: \>where $h=\T H/(i_{\it mig})$\\

2942: 

2943: %\\ ! G-moveElement5!\\

2944: \S mE16:/ \>$ pc \in \{121,123\}$\\

2945: \>$\lor~ ($\=$pc=125 \Land \neg b_{\it mE}$\\

2946: \>\>$\land~ (\S val/(w_{\it mE})=\B null/ \Lor a_{\it mE}\neq \S ADR/(w_{\it mE})))$\\

2947: \>$\implies \quad \forall m<n_{\it mE}:$\\

2948: \>\>~~$\neg \S Find/(to.\T table/[\S key/(a_{\it mE},to.\T size/,m)],a_{\it mE})$

2949: \end{tab1}

2950: 

2951: 

2952: \medbreak Invariants about the integer array \T prot/.

2953: \begin{tab1} 

2954: 

2955:  %\\ ! G-prot!\\

2956: \S pr1:/ \> $ \T prot/[i] ~=~ $\=$ \sharp (\S prSet1/(i)) ~+~ \sharp (\S prSet2/(i)) ~+~ \sharp (\T currInd/=i)$\\

2957: \>\>$ +~ \sharp (\T next/(\T currInd/)=i)$ \\

2958: 

2959:  %\\ ! G-guard1-a!\\

2960: \S pr2:/ \>$ \T prot/[\T currInd/]>0$ \\

2961: 

2962:  %\\ ! G-guard1-b!\\

2963: \S pr3:/ \>$ pc \in [1,58]\Lor pc\geq 62 \Land pc\neq 65~\implies \quad \T prot/[\S index/]>0$ \\

2964: 

2965:  %\\ ! G-guard1-next!\\

2966: \S pr4:/ \>$ \T next/(\T currInd/)\neq 0~\implies \quad \T prot/[\T next/(\T currInd/)]>0$\\

2967: 

2968:  %\\ ! G-prot2!\\

2969: \S pr5:/ \>$ \T prot/[i]=0~\implies \quad \T Heap/(\T H/[i])=\bot$ \\

2970: 

2971:  %\\ ! G-prot3!\\

2972: \S pr6:/ \>$ \T prot/[i]\leq\sharp (\S prSet3/(i)) \Land \T busy/[i]=0~\implies \quad

2973: \T Heap/(\T H/[i])=\bot$ \\

2974: 

2975:  %\\ ! G-guard4!\\

2976: \S pr7:/ \>$ pc \in [67,72]~\implies \quad \T prot/[i_{\it rA}]>0$ \\

2977: 

2978:  %\\ ! G-guard6!\\

2979: \S pr8:/ \>$ pc\in [81,84]~\implies \quad \T prot/[i_{\it nT}]>0$\\

2980: 

2981:  %\\ ! G-guard5!\\

2982: \S pr9:/ \>$ pc\geq 97~\implies \quad \T prot/[i_{\it mig}]>0$ \\

2983: 

2984:  %\\ ! G-prot4!\\

2985: \S pr10:/ \>$ pc\in [81,82]~\implies \quad \T prot/[i_{\it nT}]=\sharp (prSet4(i_{\it nT}))+1$

2986: \end{tab1}

2987: 

2988: 

2989: \medbreak Invariants about the integer array \T busy/.

2990: 

2991: \begin{tab1} 

2992:  %\\ ! G-busysize,G-busy!\\

2993: \S bu1:/ \> $ \T busy/[i] ~=~ $\=$\sharp (buSet1(i)) ~+~ \sharp (buSet2(i)) ~+~ \sharp (\T currInd/=i)$\\

2994: \>\>$ +~ \sharp (\T next/(\T currInd/)=i) $\\

2995: 

2996:  %\\ ! G-guard2-a!\\

2997: \S bu2:/ \>$ \T busy/[\T currInd/]>0$\\

2998: 

2999:  %\\ ! G-guard2-b!\\

3000: \S bu3:/ \>$ pc \in [1,58]$\\

3001: \>$\lor~ pc>65 \Land \neg(i_{\it rA}=\S index/ \Land pc \in [67,72])$\\

3002: \>$\implies \quad \T busy/[\S index/]>0$\\

3003: 

3004:  %\\ ! G-busy1-next!\\

3005: \S bu4:/ \>$ \T next/(\T currInd/)\neq 0~\implies \quad \T busy/[\T next/(\T currInd/)]>0$\\

3006: 

3007:  %\\ ! G-guard7!\\

3008: \S bu5:/ \>$ pc=81~\implies \quad \T busy/[i_{\it nT}]=0$\\

3009: 

3010:  %\\ ! G-guard3!\\

3011: \S bu6:/ \>$ pc\geq 100~\implies \quad \T busy/[i_{\it mig}]>0$

3012: \end{tab1}

3013: 

3014: 

3015: \medbreak Some other invariants we have postulated:

3016: 

3017: \begin{tab1} 

3018: %\\ ! G-ADR2!\\

3019: \S Ot1:/ \>$ \T X/(\B 0/)=\B null/$\\

3020: %\\ ! G-ADR1!\\

3021: \S Ot2:/ \>$ \T X/(a)\neq \B null/~\implies \quad \S ADR/(\T X/(a))=a$

3022: \end{tab1}

3023: The motivation of invariant (Ot1) is that we never store a value for 

3024: the address 0.

3025: The motivation of invariant (Ot2) is that the address in the hash table 

3026: is unique. 

3027: 

3028: \begin{tab1} %\\ ! G-R1!\\

3029: \S Ot3:/ \>$ return_{\it gA}=\{1, 10, 20, 30, 36, 46, 51\} \Land

3030: return_{\it rA}=\{0, 59, 77, 90\}$ \\

3031: \>$\land~ return_{\it ref}=\{10, 20, 30, 36, 46, 51\} \Land

3032: return_{\it nT}=\{30, 46\}$ 

3033: \end{tab1}

3034: 

3035: \begin{tab1} 

3036: %\\ ! G-pc!\\

3037: \S Ot4:/ \>$ pc\in \{$\=$0,~1,~5,~6,~7,~8,~10,~11,~13,~14,~15,~

3038: 16,~17,~18,~20,~$\\

3039: \>\>$21,~25,~26,~27,~28,~30,~31,~32,~33,~35,~36,~37,~41,~$\\

3040: \>\>$42,~43,~44,~46,~47,~48,~49,~50,~51,~52,~57,~59,~60,~$\\

3041: \>\>$61,~62,~63,~65,~67,~68,~69,~70,~71,~72,~77,~78,~81,~$\\

3042: \>\>$82,~83,~84,~90,~94,~95,~97,~98,~99,~100,~101,~102,~$\\

3043: \>\>$103,~104,~105,~110,~111,~114,~116,~117,~118,~120,~$\\

3044: \>\>$121,~123,~125,~126\}$

3045: \end{tab1}

3046: 

3047: \section{Dependencies between invariants}

3048: Let us write ``$\phi\ \B from/\ \psi_1, \cdots, \psi_n $'' to denote 

3049: that $\phi$ is proved to be an invariant using that $\psi_1$, \dots, 

3050: $\psi_n $ hold.

3051: We write ``$\phi\ \Leftarrow\ \psi_1, \cdots, \psi_n $'' to denote 

3052: that predicate $\phi$  is implied by the conjunction of  $\psi_1$, 

3053: \dots, $\psi_n $.

3054: We have verified the following ``\B from/'' and ``$\Leftarrow $'' 

3055: relations mechanically:

3056: 

3057: \begin{tab}

3058: Co1 \B from/ fi10, Ot3, fi1\\

3059: Co2 \B from/ de5, Ot3, de6, del, de11\\

3060: Co3 \B from/ in5, Ot3, in6, in1, in11\\

3061: Cn1 \B from/ Cn6, Ot3\\

3062: Cn2 \B from/ Cn8, Ot3, del\\

3063: Cn3 \B from/ Cn10, Ot3, in1, in5\\

3064: Cn4 \B from/ Cn11, Ot3\\

3065: No1 $\Leftarrow $ No2\\

3066: No2 \B from/ nT1, He2, rA2, Ot3, Ha2, Ha1, rA1, rA14, rA3, nT14, rA4\\

3067: He1 \B from/ Ha1\\

3068: He2 \B from/ Ha3, rA5, Ha1, He1, rA2\\

3069: He3, He4 \B from/ Ot3, rA6, rA7, mi12, rA11, rA5\\

3070: He5 \B from/ He1\\

3071: He6 \B from/ rA8, Ha3, mi8, nT2, rA5\\

3072: Ha1 \B from/ true\\

3073: Ha2 \B from/ Ha1\\

3074: Ha3 \B from/ Ha2, Ha1, He2, He1\\

3075: Ha4 $\Leftarrow $ Ha3, He3, He4\\

3076: Cn5 \B from/ Cn6, Ot3 \\

3077: Cn6 \B from/ Cn5, Ot3\\

3078: Cn7 \B from/ Cn8, Ot3, del\\

3079: Cn8 \B from/  Cn7, Ot3 \\

3080: Cn9 \B from/  Cn10, Ot3, in1, in5\\

3081: Cn10 \B from/ Cn9, Ot3, in5\\

3082: Cn11 \B from/ Cn11, Ot3\\

3083: Cu1 \B from/ Ot3, Ha4, rA6, rA7, nT13, nT12, Ha2, He3, He4, rA11, nT9, nT10,\\

3084:   \> mi13, rA5\\

3085: Cu2 $\Leftarrow $ Cu6, cu7, Cu3, He3, He4\\

3086: Cu3 \B from/ rA6, rA7, nT13, nT12, mi5, mi4, Ne8, rA5\\

3087: Cu4 \= \B from/ del, in1, as1, rA6, rA7, Ha2, nT13, nT12, Ne9, Cu9, Cu10, de7, \\

3088:   \> in7, as5, He3, He4, mi5, mi4, Ot3, Ha4, de3, mi9, mi10, de5, rA5\\

3089: Cu6 \= \B from/ Ot3, rA6, rA7, Ha2, nT13, nT12, Ha3, in3, as3, Ne23, mi5, mE6,\\

3090:   \> mE7, mE10, mE3, Ne3, mi1, mi4, rA5\\

3091: Cu7 \= \B from/ Ot3, rA6, rA7, Ha2, nT13, nT12, Ha3, in3, as3, in5, mi5, mE6, \\

3092:     \> mE7, mE10, mE3, Ne3, mi4, de7, in7, as5, Ne22, mi9, mi10, rA5, He3, \\

3093:     \> mi12, mi1, Cu9, de1 in1, as1\\

3094: Cu8 \= \B from/ Cu8, Ha2, nT9, nT10, rA6, rA7, mi5, mi4, mC2, mC5, He3,\\

3095:     \> He4, Cu1, Ha4, mC6, mi16, rA5\\

3096: Cu9\=, Cu10 \B from/ rA6, rA7, nT13, nT12, Ha2, He3, He4, Cu1, Ha4, de3, in3,\\

3097:  \> as3, mE3, mi9, mi10, mE10, mE7, rA5\\

3098: Cu11\=, Cu12 \B from/ Cu9, Cu10, Cu13, Cu14, del, in1, as1, rA6, rA7, Ha2, nT13,\\

3099:  \> nT12, He3, He4, Cu1, Ha4, in3, as3, mi14, mi15, de3, in10, as8, mi12, \\

3100:  \> Ot2, fi5, de8, in8, as6, Cu15, de11, in11, rA5\\

3101: Cu13\=, Cu14 \B from/ He3, He4, Ot2, del, in1, as1, Ot1, rA6, rA7, nT13, nT12, \\

3102:     \> Ha2, Cu9, Cu10, Cu1, Ha4, de3, in3, as3, Cu11, Cu12, in10, as8, fi5, de8, \\

3103:     \> in8, as6, Cu15, mi17, mi18, mi12, mi4, de11, rA5\\

3104: Cu15\=\ \B from/ He3, He4, rA6, rA7, nT13, nT12, Ha2, Cu1, Ha4, del, in1, as1,\\

3105:     \> de3, in3, as3, fi5, de8, in8, as6, mi12, mi19, mi4, Ot2, Cu9, Cu10, Cu11, \\

3106:     \> Cu12, Cu13, Cu14, rA5 \\

3107: Cu16 $\Leftarrow $ Cu13, Cu14, Cu15, He3, He4, Ot1\\

3108: Ne1 \B from/ nT9, nT10, mi7\\

3109: Ne2 \B from/ Ne5, nT3, mi8, nT9, nT10\\

3110: Ne3 \B from/ Ne1, nT9, nT10, mi8\\

3111: Ne4 \B from/ Ne1, nT9, nT10\\

3112: Ne5 \B from/ Ot3, nT9, nT10, mi5\\

3113: Ne6 $\Leftarrow $ Ne10, Ne24, He6, He3, He4, Cu4\\

3114: Ne7 \B from/ Ha3, rA6, rA7, rA8, nT13, nT12, nT11, He3, He4, mi8, nT7, \\

3115:     \> Ne5, Ha2, He6, rA5\\

3116: Ne8 \B from/ Ha3, rA8, nT11, mi8, nT6, Ne5, rA5\\

3117: Ne9 \B from/ Ha3, Ha2, Ne3, Ne5, de3, as3, rA8, rA6, rA7, nT8, nT11, mC2, \\

3118:     \> nT4, mi8, rA5\\

3119: Ne9a \B from/ Ha3, Ne3, rA5, de3, rA8, nT4, mi8\\

3120: Ne10 \B from/ Ha3, Ha2, de3, rA8, nT11, Ne3, He6, mi8, nT8, mC2, nT2, Ne5, \\

3121:     \> rA5\\

3122: Ne11 \B from/ Ha3, Ha2, He6, nT2, nT8, rA8, nT11, mi8, Ne3, mC2, rA5\\

3123: Ne12\=, Ne13 \B from/ Ha3, Ha2, Cu8, He6, He3, He4, Cu1, de3, in3, as3, rA8, rA6, \\

3124:     \> rA7, nT11, nT13, nT12, mi12, mi16, mi5, mi4, de7, in7, as5, Ot2, del,in1, \\

3125:     \> as1, Cu9, Cu10, Cu13, Cu14, Cu15, as9, fi5, de8, in8, as6, mC2, Ne3, Ot1, \\

3126:     \> Ne14, Ne20, mE16, mE7, mE4, mE1, mE12, mE2, Ne15, Ne16, Ne17,\\

3127:     \> Ne18, mi20, de11, in11, rA5 \\

3128: Ne14\=\ \B from/ Ha3, Ha2, He6, He3, He4, nT2, nT8, de3, in3, as3, rA8, nT11,\\

3129:     \> Ot2, del, in1, as1, Cu9, Cu10, mi8, Ne3, mC2, mE7, mE16, mE1, mE4, \\

3130:     \> mE12, Ne17, Ne18, Cu1, rA5\\

3131: Ne15\=, Ne16 \B from/ Ha3, Ha2, Cu8, He6, He3, He4, Cu1, de3, in3, as3, rA8, rA6, \\

3132:     \> rA7, nT11, nT13, nT12, mi12, mi16, mi5, mi4, de7, in7, as5, Ot2, del, in1, \\

3133:     \> as1, Cu9, Cu10, Cu13, Cu14, Cu15, as9, fi5, de8, in8, as6, mC2, Ne3, Ot1, \\

3134:     \> Ne19, Ne20, Ne12, Ne13, mE16, mE7, mE4, mE1, mE12, mE10, mE2, \\

3135:     \> in11, de11, rA5\\

3136: Ne17\=, Ne18 \B from/ Ha3, Ha2, mi8, He6, He3, He4, Cu1, nT2, de3, in3, as3, rA8,\\

3137:     \> rA6, rA7, nT11, nT13, nT12, de7, in7, as5, Ot2, del, in1, as1, Cu9, Cu10, \\

3138:     \> nT8, mE2, fi5, de8, in8, as6, mC2, Ne3, mC11, mC6, mC12, mE7, mE10,\\

3139:     \> mE1, Cu8, Cu15, Cu13, Cu14, Cu11, Cu12, as8, de11, rA5\\

3140: Ne19\=\ \B from/ Ha3, Ha2, He6, nT2, nT8, de3, in3, as3, rA8, nT11, mi8, Ne3, \\

3141:     \> mE7, Ne14, mE16, Ot1, mE1, mE4, mE12, Ne17, Ne18, rA5\\

3142: Ne20\=\ \B from/ Ha3, Ha2, Cu8, He6, He3, He4, Cu1, Ha4, de3, in3, as3, rA8, rA6,\\

3143:     \> rA7, nT11, nT13, nT12, mi12, mi16, mi5, mi4, Ne1, de7, in7, as5, del, in1,\\

3144:     \> as1, Cu9, Cu10, Cu13, Cu14, Cu15, as9, fi5, de8, in8, as6, mC2, Ne3, Ot1,\\

3145:     \> mi20, in11, rA5\\

3146: Ne22\=\ \B from/ Ot3, rA8, Ha2, nT11, Ha3, de3, in3, as3, mi5, mi4, Ne3, nT18,\\

3147:     \> mE3, mi8, mE10, mE7, mE6, Ne5, nT5, nT2, rA5, nT8, nT12, mC2, mE2\\

3148: Ne23 $\Leftarrow $ Cu6, cu7, Ne6, Ne7, He3, He4, Ne22, He6\\

3149: Ne24 $\Leftarrow $ Ne27, He6 \\

3150: Ne25 $\Leftarrow $ Ne19, Ne17, Ne18, He6 \\

3151: Ne26 $\Leftarrow $ Ne17, Ne18, He6\\

3152: Ne27 $\Leftarrow $ Cu16, Ne25, Ne26, Ne17, Ne18, He6 \\

3153: fi1, del, in1, as1 \B from/ \\

3154: fi2 \B from/ fi2, Ot3 \\

3155: fi3 \B from/ fi4, Ot3, rA6, rA7, Ha2, rA5\\

3156: fi4 \B from/ Ot3, rA6, rA7, nT13, nT12 \\

3157: fi5, de8, in8, as6 $\Leftarrow $ Cu2, de10, in10, as8, fi8, He3, He4\\

3158: fi6 \= \B from/ Ot3, fi1, del, in1, as1, rA6, rA7, Ha2, nT13, nT12, mi9, mi10, Cu9, \\

3159:     \> Cu10, He3, He4, Cu1, Ha4, fi4, in3, as3, rA5\\

3160: fi7 \= \B from/ fi8, fi6, fi2, Ot3, fi1, del, in1, as1, rA6, rA7, Ha2, nT13, nT12, mi9, \\

3161:     \> mi10, Cu9, Cu10, He3, He4, Cu1, Ha4, fi4, in3, as3, rA5\\

3162: fi8 \= \B from/ fi4, fi7, fi2, Ot3, fi1, del, in1, as1, rA6, rA7, Ha2, nT13, nT12, mi9,\\

3163:     \> mi10, Cu9, Cu10, He3, He4, Cu1, Ha4, in3, as3, rA5\\

3164: fi9 \= $\Leftarrow $ Cu1, Ha4, Cu9, Cu10, Cu11, Cu12, fi8, fi3, fi4, fi5, de8, in8, \\

3165:     \> as6, He3, He4\\

3166: fi10 \B from/ fi9, Ot3\\

3167: fi11\=, de12, in12, as10 \B from/ Ot3, nT9, nT10, mi9, mi10, Cu8, fi4, de3, in3, \\

3168:     \> as3, fi3, de2, in2, as2\\

3169: de2 \B from/ de3, Ot3, rA6, rA7, Ha2, rA5\\

3170: de3 \B from/ Ot3,  rA6, rA7, nT13, nT12 \\

3171: de4, in4, as4 \B from/ Ot3\\

3172: de5 \B from/ Ot3 \\

3173: de6 \B from/ Ot3, de1, de11 \\

3174: de7, in7, as5 $\Leftarrow $ de3, in3, as3, Cu1, Ha4, de13, in13, as11\\

3175: de9 \= \B from/ Ot3, del, in1, as1, rA6, rA7, Ha2, nT13, nT12, mi9, mi10, \\

3176:     \> Cu9, Cu10, de3, de7, in7, as5, rA5\\

3177: de10\=\ \B from/ de3, de9, Ot3, del, in1, as1, rA6, rA7, Ha2, nT13, nT12, mi9, \\

3178:     \> mi10, Cu9, Cu10, de7, in7, as5, He3, He4, rA5\\

3179: de11 $\Leftarrow $ de10, de2, de3, He3, He4, Cu1, Ha4, Cu9, Cu10, Cu11, Cu12, fi5, \\

3180:     \> de8, in8, as6 \\

3181: de13, in13, as11 $\Leftarrow $ Ax2, de2, de3, de4, in2, in3, in4, as2, as3, as4\\

3182: in2 \B from/ in3, Ot3, rA6, rA7, Ha2, rA5\\

3183: in3 \B from/ Ot3, rA6, rA7, nT13, nT12\\

3184: in5 \B from/ Ot3\\

3185: in6 \B from/ Ot3, in1, in11\\

3186: in9 \= \B from/ Ot3, del, in1, as1, rA6, rA7, Ha2, nT13, nT12, mi9, mi10, Cu9,\\

3187:     \> Cu10, He3, He4, in3, de7, in7, as5, rA5\\

3188: in10\=\ \B from/ in9, fi2, Ot3, del, in1, as1, rA6, rA7, Ha2, nT13, nT12, mi9, mi10, \\

3189:     \> Cu9, Cu10, He3, He4, in3, de7, in7, as5, rA5\\

3190: in11 $\Leftarrow $ in10, in2, in3, Cu1, Ha4, Cu9, Cu10, Cu11, Cu12, fi5, de8, in8, as6 \\

3191: as2 \B from/ as3, He3, He4, Ot3, rA6, rA7, Ha2, rA5\\

3192: as3 \B from/ Ot3, rA6, rA7, nT13, nT12 \\

3193: as7 \= \B from/ Ot3, del, in1, as1, rA6, rA7, Ha2, nT13, nT12, mi9, mi10, Cu9, \\

3194:     \> Cu10, as3, de7, in7, as5, rA5\\

3195: as8 \= \B from/ as7, Ot3, del, in1, as1, rA6, rA7, Ha2, nT13, nT12, mi9, mi10, Cu9, \\

3196:     \> Cu10, He3, He4, as3, de7, in7, as5, rA5\\

3197: as9 $\Leftarrow $ as8, as2, as3, He3, He4, Cu1, Ha4, Cu9, Cu10, Cu11, Cu12, fi5, de8,\\

3198:     \> in8, as6 \\

3199: rA1 \B from/ Ha2\\

3200: rA2 \B from/ Ot3\\

3201: rA3 \B from/ Ot3, rA9, He2, He1, rA2, rA13 \\

3202: rA4 \B from/ Ot3, nT14\\

3203: rA5 \B from/ Ot3, rA1, rA2, Ha3, He2\\

3204: rA6\=, rA7 \B from/ Ot3, nT13, nT12, nT14, rA11, mi4, bu2, bu3, Ha3, mi6, Ha2,\\

3205:     \> He3, He4, He2, rA2\\

3206: rA8 \B from/ Ot3, bu4, nT14, mi6, Ne2, mi5\\

3207: rA9 \B from/ Ot3, Ha2, nT14, He1, He2\\ 

3208: rA10 \B from/ Ot3\\

3209: rA11 \B from/ Ot3, nT13, nT12, mi2\\

3210: rA12 \B from/ Ot3, nT9, nT10\\

3211: rA13 \B from/ Ot3, rA5\\

3212: rA14 \B from/ Ot3, rA4, He1, rA2\\

3213: nT1 \B from/ Ot3, pr5, Ha3, nT14, nT16, Ha2\\

3214: nT2 \B from/ Ot3, nT14, Ha3, rA5\\

3215: nT3 \B from/ Ot3, nT9, nT10\\

3216: nT4 \B from/ Ot3, Ha3, de3, nT13, nT12, nT15, rA5\\

3217: nT5 \B from/ Ot3, Ha3, in3, as3, nT13, nT12, nT15, nT18, mE3, mi4, rA5\\

3218: nT6 \B from/ Ot3, nT13, nT12, nT14, Ha3, rA5\\

3219: nT7 \B from/ Ot3, nT13, nT12, nT15, rA6, rA7, Ha2, mi9, mi10, nT14, Ha3, \\

3220:     \> nT16, rA5\\

3221: nT8 \= \B from/ Ot3, de3, in3, as3, nT13, nT12, nT15, nT18, mE3, mi4, Ha3, mC2,\\

3222:     \> nT16, nT2, Ha2, rA5\\

3223: nT9, nT10 \B from/ Ot3, pr2, pr3, nT18 \\

3224: nT11 \B from/ Ot3, pr4, nT16, mi8\\

3225: nT13, nT12 $\Leftarrow $ nT9, nT10, Ha3, He3, He4\\

3226: nT14 \B from/ Ot3, nT9, nT10, nT18, nT16, pr7\\

3227: nT15 $\Leftarrow $ nT14, Ha3, nT2\\

3228: nT16 \B from/ Ot3, pr8\\

3229: nT17 \B from/ Ot3, mi5, pr4, nT11, mi10\\

3230: nT18 \B from/ Ot3, pr9, mi5, nT11\\

3231: mi1 \B from/ Ot3, mi9, mi10, mi10\\

3232: mi2 \B from/ Ot3, Ne4\\

3233: mi3 \B from/ Ot3, fi11, de12, in12, as10, nT9, nT10, Ne5\\

3234: mi4 \B from/ Ot3, mi9, mi10, mi3\\

3235: mi5 \B from/ Ot3, nT9, nT10, Ne5, mi10, mi4\\

3236: mi6 \B from/ Ot3, mi5, bu6, rA8, mi9, mi10, bu4, mi4\\

3237: mi7 \B from/ Ot3, mi2, mi7, mi4, nT18, Ne2, mi10, nT17, mi3\\

3238: mi8 \B from/ Ot3, mi10, Ne2, mi3\\

3239: mi9,\=\ mi10 \B from/ Ot3, He3, He4, nT9, nT10, nT18, Ne3, Ha3, mi3, nT17, \\

3240:     \> mi10, He2, mi4, mi12, mi6, He6 \\

3241: mi11 \B from/ Ot3, nT18, mi9, mi6, mi6\\

3242: mi12 \B from/ Ot3, rA8, nT2, He6, mi9, mi5, mi3, Ha3, mi4, rA5\\

3243: mi12 \B from/ Ot3, mi12, nT18, mi6, Ha3, mi4, rA5\\

3244: mi13 \B from/ Ot3, rA6, rA7, Ha2, nT13, nT12, He3, He4, mi9, mi10, mC9, rA5\\

3245: mi14\=, mi15 $\Leftarrow $ Ne12, Ne13, mi5, Cu15, mi13, Ot2, He3, He4, Ne17, Ne18,\\

3246:     \> Cu8, He6, He5, mi4, Ot1\\ 

3247: mi16 $\Leftarrow $ Ne11, mi5, mi4 \\

3248: mi17, mi18 $\Leftarrow $ Ne15, Ne16, mi5, Cu15, mi13, Ot2, He3, He4, Ne17, Ne18, \\

3249:     \> Cu8, He6, He5, mi4\\

3250: mi19 $\Leftarrow $ Ne20, mi5, Cu15, mi13, Ot2, He3, He4\\

3251: mi20 \=\ \B from/ Ha3, Ha2, Cu8, He6, He3, He4, Cu1, Ha4, de3, in3, as3, rA8, \\

3252:      \> rA6, rA7, nT11, nT13, nT12, mi5, mi4, de7, in7, as5, Ot2, del, in1, \\

3253:      \> as1, Cu9, Cu10, Cu13, Cu14, Cu15, as9, fi5, de8, in8, as6, mC6, Ne3,\\

3254:      \> Ot3, mC11, mi13, mi9, mi10, mC2, mE3, mE10, mE7, mC12, mE1, \\

3255:      \> mE13, Ne17, Ne18, mE2, mE4, Ot1, mE6, Ne10, in11, rA5\\

3256: mC1 \B from/ Ot3, mi6, mi11, nT18 \\

3257: mC2 \B from/ Ot3, rA6, rA7, nT13, nT12, mC2\\

3258: mC3 \B from/ Ot3, mC3, nT13, nT12, rA6, rA7, Ha2, rA5\\

3259: mC4 \B from/ Ot3, mC4, mC2, mC3, He3, He4, rA6, rA7, Ha2, rA5\\

3260: mC5 \B from/ Ot3 \\

3261: mC6 \B from/ Ot3, rA6, rA7, Ha2, nT13, nT12, mC2, rA5\\

3262: mC7 \B from/ Ot3, rA6, rA7, Ha2, nT13, nT12, mC2, rA5\\

3263: mC8 \B from/ Ot3, rA6, rA7, Ha2, nT13, nT12, He3, He4, mC7, rA5\\

3264: mC9 \B from/ Ot3, rA6, rA7, Ha2, nT13, nT12, He3, He4, mi9, mi10, He5, \\

3265:     \> mC7, mC8, rA5\\

3266: mC10\=\ \B from/ Ot3, rA6, rA7, Ha2, nT13, nT12, mC2, del, in1, as1, mi6,\\

3267:     \> Ha3, mi4, nT18, mE15, mC11, mi5, rA5\\

3268: mC11 \B from/ Ot3, rA6, rA7, Ha2, nT13, nT12, mC2, rA5\\

3269: mC12 \B from/ Ot3, rA6, rA7, mC2, mC11, Cu9, Cu10, de7, in7, as5, mi9,\\

3270:      \> mC6 \\ 

3271: mE1 \B from/ Ot3 \\

3272: mE2 \B from/ Ot3 \\

3273: mE3 \B from/ mC1, Ot3, mi6, nT18 \\

3274: mE4 \B from/ Ot3, mE1\\

3275: mE5 \B from/ Ot3, mE3, Ha3, mi6, mi4, nT18, Ha2, rA5\\

3276: mE6 \B from/ Ot3 \\

3277: mE7 \B from/ Ot3, Ha2, Ha3, mi6, mi4, mE3, rA5\\

3278: mE8 \B from/ Ot3, Ha3, mi6, mi4, nT18, Ha2, mE3, rA5\\

3279: mE9 \= \B from/ Cu1, Ha4, Ot3, Ha2, Ha3, mi6, mi4, mE3, mC2, mC10, mE1, \\

3280:     \> mC1, del, in1, as1, mi13, mi12, mC6, mE2, rA5\\

3281: mE10 \B from/ del, in1, as1, mE3, mi6, Ot3, Ha2, Ha3, mi4, mE11, mE9,\\

3282:     \> mE7, rA5\\

3283: mE11\=\ $\Leftarrow $ mE10, mi13, mE16, mi16, mi5, mE3, Ne12, Ne13, mC12, mE2,\\

3284:     \> mE1, mE4, mC6, mE12, mi12, Cu13, Cu14, He3, He4, mi4\\

3285: mE12 $\Leftarrow $ Ne23, Ne22, mE16, He6, Ne8\\

3286: mE13 \B from/ Ot3, Ha2, mE14, del, in1, as1, Ha3, mi6, mi4, mE3, rA5\\

3287: mE14 \B from/ Ot3, Ha2, del, in1, as1, Ha3, mi6, mi4, nT18, mE3, mE2, rA5\\

3288: mE15\=\ \B from/ Ot3, mE1, Ha2, del, in1, as1, Ha3, mi6, mi4, nT18, mE3, mE2,\\

3289:     \> mE7, mE14, mE4, rA5\\

3290: mE16\=\ \B from/ Ha3, Ha2, mE3, del, in1, as1, mi6, mE2, mE4, mE1, mE7, mi4,\\

3291:     \> Ot3, mE14, mE13, rA5\\

3292: pr1 \B from/ Ot3, rA11, rA10, nT9, nT10, Ne5, mi2, mi4, mi8, mi5\\

3293: pr2, pr3 \B from/ pr1, Ot3, rA11, mi1 \\

3294: pr4 $\Leftarrow $ pr1\\

3295: pr5 $\Leftarrow $ pr6, pr1, bu1\\

3296: pr6 \B from/ Ot3, Ha2, nT9, nT10, nT14, nT16, He2, rA2, pr1, bu1, pr10, \\

3297:     \> rA9, He1, rA4\\

3298: pr7, pr8, pr9 $\Leftarrow $ pr1, mi4\\

3299: pr10 \B from/ Ot3, pr1, nT9, nT10, nT14, nT17\\

3300: bu1 \B from/ Ot3, rA11, rA10, nT9, nT10, Ne5, mi2, mi8, mi5, bu5\\

3301: bu2, bu3 $\Leftarrow $ bu1, Ot3, rA10\\

3302: bu4 $\Leftarrow $ bu1\\

3303: bu5 \B from/ Ot3, nT9, nT10, nT16, nT18, pr1, bu1\\

3304: bu6 $\Leftarrow $ bu1, mi4\\

3305: Ot1 \B from/ del, in1, as1\\

3306: Ot2 \B from/ del, in1, as1\\

3307: Ot3 \B from/ true\\

3308: Ot4 \B from/ Ot3\\

3309: \end{tab}

3310: 

3311: \begin{thebibliography}{10}

3312: 

3313: \bibitem{ARJ97}

3314: J.H. Anderson, S.~Ramamurthy, and K.~Jeffay.

3315: \newblock Real-time computing with lock-free shared objects.

3316: \newblock {\em ACM Trans. Comput. Syst.}, 15(2):134--165, 1997.

3317: 

3318: \bibitem{ABD90}

3319: H.~Attiya, A.~Bar-Noy, D.~Dolev, D.~Peleg, and R.~Reischuk.

3320: \newblock Renaming in an asynchronous environment.

3321: \newblock {\em Journal of the ACM}, 37:524--548, 1990.

3322: 

3323: \bibitem{BD89}

3324: A.~Bar-Noy and D.~Dolev.

3325: \newblock Shared-memory vs.\ message-passing in an asynchronous distributed

3326:   environment.

3327: \newblock In {\em Proc.\ 8th ACM Symp.\ on principles of distributed

3328:   computing}, pages 307--318, 1989.

3329: 

3330: \bibitem{Bar93}

3331: G.~Barnes.

3332: \newblock A method for implementing lock-free shared-data structures.

3333: \newblock In {\em Proceedings of the fifth annual ACM symposium on Parallel

3334:   algorithms and architectures}, pages 261--270. ACM Press, 1993.

3335: 

3336: \bibitem{FCB00}

3337: F.~Cassez, C.~Jard, B.~Rozoy, and M.~Dermot.

3338: \newblock Modeling and verification of parallel processes, 2000.

3339: \newblock 4th Summer School, MOVEP 2000, Nantes, France.

3340: 

3341: \bibitem{HesMv}

3342: H.~Gao, J.F. Groote, and W.H. Hesselink.

3343: \newblock {PVS} verification.

3344: \newblock \\\verb!http://www.cs.rug.nl/~wim/mechver/hashtable!, 2003.

3345: 

3346: \bibitem{Jan00}

3347: J.F. Groote, W.H. Hesselink, S.~Mauw, and R.~Vermeulen.

3348: \newblock An algorithm for the asynchronous write-all problem based on process

3349:   collision.

3350: \newblock {\em Distr. Comput.}, 14:75--81, 2001.

3351: 

3352: \bibitem{Har92}

3353: S.P. Harbison.

3354: \newblock {\em Modula-3}.

3355: \newblock Prentice Hall, New Yersey, 1992.

3356: 

3357: \bibitem{Her91}

3358: M.~Herlihy.

3359: \newblock Wait--free synchronization.

3360: \newblock {\em ACM Trans. Program. Lang. Syst.}, 13:124--149, 1991.

3361: 

3362: \bibitem{Her93}

3363: M.~Herlihy.

3364: \newblock A methodology for implementing highly concurrent data objects.

3365: \newblock {\em ACM Trans. Program. Lang. Syst.}, 15:745--770, 1993.

3366: 

3367: \bibitem{HeW90}

3368: M.~Herlihy and J.~Wing.

3369: \newblock Linearizability: a correctness condition for concurrent objects.

3370: \newblock {\em ACM Trans. Program. Lang. Syst.}, 12:463--492, 1990.

3371: 

3372: \bibitem{HeM92}

3373: M.P. Herlihy and J.E.B. Moss.

3374: \newblock Lock-free garbage collection for multiprocessors.

3375: \newblock {\em IEEE Transactions on Parallel and Distributed Systems},

3376:   3:304--311, 1992.

3377: 

3378: \bibitem{H95}

3379: W.H. Hesselink.

3380: \newblock Wait--free linearization with a mechanical proof.

3381: \newblock {\em Distr. Comput.}, 9:21--36, 1995.

3382: 

3383: \bibitem{H96}

3384: W.H. Hesselink.

3385: \newblock Bounded delay for a free address.

3386: \newblock {\em Acta Inf.}, 33:233--254, 1996.

3387: 

3388: \bibitem{HG99}

3389: W.H. Hesselink and J.F. Groote.

3390: \newblock Wait-free concurrent memory management by {C}reate, and {R}ead until

3391:   {D}eletion ({CaRuD}).

3392: \newblock {\em Distr. Comput.}, 14:31--39, 2001.

3393: 

3394: \bibitem{KS97}

3395: P.C. Kanellakis and A.A. Shvartsman.

3396: \newblock {\em Fault-tolerant parallel computation}.

3397: \newblock Kluwer Academic Publishers, Dordrecht, 1997.

3398: 

3399: \bibitem{Knuth3}

3400: D.E. Knuth.

3401: \newblock {\em The Art of Computer Programming. Part 3, Sorting and searching}.

3402: \newblock Addison-Wesley, 1973.

3403: 

3404: \bibitem{LaMa94}

3405: A.~LaMarca.

3406: \newblock A performance evaluation of lock-free synchronization protocols.

3407: \newblock In {\em Proceedings of the thirteenth annual ACM symposium on

3408:   Principles of distributed computing}, pages 130--140. ACM Press, 1994.

3409: 

3410: \bibitem{Lam94}

3411: L.~Lamport.

3412: \newblock The temporal logic of actions.

3413: \newblock {\em ACM Trans. Program. Lang. Syst.}, 16:872--923, 1994.

3414: 

3415: \bibitem{Lyn96}

3416: N.A. Lynch.

3417: \newblock {\em Distributed Algorithms}.

3418: \newblock Morgan Kaufman, San Francisco, 1996.

3419: 

3420: \bibitem{ZA92}

3421: Z.~Manna and A.~Pnueli.

3422: \newblock {\em The Temporal Logic of Reactive and Concurrent Systems:

3423:   Specification}.

3424: \newblock Springer, New York, 1992.

3425: 

3426: \bibitem{Mic02}

3427: M.M. Michael.

3428: \newblock High performance dynamic lock-free hash tables and list-based sets.

3429: \newblock In {\em Proceedings of the fourteenth annual ACM symposium on

3430:   Parallel algorithms and architectures}, pages 73--82. ACM Press, 2002.

3431: 

3432: \bibitem{OSR01}

3433: S.~Owre, N.~Shankar, J.~M. Rushby, and D.~W.~J. Stringer-Calvert.

3434: \newblock {\em PVS Version 2.4, System Guide, Prover Guide, PVS Language

3435:   Reference}, 2001.

3436: \newblock \verb!http://pvs.csl.sri.com!

3437: 

3438: \bibitem{RaG02}

3439: R.~Rajwar and J.R. Goodman.

3440: \newblock Transactional lock-free execution of lock-based programs.

3441: \newblock In {\em Tenth international conference on architectural support for

3442:   programming languages and operating systems on Proceedings of the 10th

3443:   international conference on architectural support for programming languages

3444:   and operating systems (ASPLOS-X)}, pages 5--17. ACM Press, 2002.

3445: 

3446: \bibitem{ShS03}

3447: O.~Shalev and N.~Shavit.

3448: \newblock Split-ordered lists: lock-free extensible hash tables.

3449: \newblock In {\em Proceedings of the twenty-second annual symposium on

3450:   Principles of distributed computing}, pages 102--111. ACM Press, 2003.

3451: 

3452: \bibitem{SuT04}

3453: H.~Sundell and P.~Tsigas.

3454: \newblock Scalable and lock-free concurrent dictionaries.

3455: \newblock In {\em Proceedings of the 2004 ACM symposium on Applied computing},

3456:   pages 1438--1445. ACM Press, 2004.

3457: 

3458: \bibitem{Valois92}

3459: J.D. Valois.

3460: \newblock Implementing lock-free queues.

3461: \newblock In {\em Proceedings of the seventh international conference on

3462:   Parallel and Distributed Computing Systems}, pages 64--69, 1994.

3463: 

3464: \bibitem{Valois94}

3465: J.D. Valois.

3466: \newblock Lock-free linked lists using compare-and-swap.

3467: \newblock In {\em Proceedings of the fourteenth annual ACM symposium on

3468:   Principles of distributed computing}, pages 214--222. ACM Press, 1995.

3469: \newblock See also J.D.~Valois. ERRATA. Lock-free linked lists using

3470:   compare-and-swap. Unpublished manuscript, 1995.

3471: 

3472: \bibitem{Wir}

3473: N.~Wirth.

3474: \newblock {\em Algorithms $+$ Data Structures $=$ Programs}.

3475: \newblock Prentice Hall, 1976.

3476: 

3477: \end{thebibliography}

3478: 

3479: \end{document}

3480: