Verifying a Wait Free RegisterAlgorithm Using AssertionalReasoningXu QiwenUniversityofMacau
Verifying a Wait Free Register Algorithm Using Assertional Reasoning Xu Qiwen University of Macau
Read and Write Conflict (Race)If read and write operations are performed onthe same memory cell at the same time, readoperation may obtain an erroneous value
Read and Write Conflict (Race) If read and write operations are performed on the same memory cell at the same time, read operation may obtain an erroneous value
Avoiding Race One cell, waiting neededwritereadMore cells, wait free possible2 cells, read and write differentwritereadcells.butreadandwritehavencrelations(read shouldreadvalueswritten by write)writeread4cells.readcanreadacellthathasbeenwrittenrecentlybutCurrently not written
Avoiding Race ⚫ One cell, waiting needed ⚫ More cells, wait free possible write read write read write read 2 cells, read and write different cells, but read and write have no relations (read should read values written by write) 4 cells, read can read a cell that has been written recently but Currently not written
Simpson 4 Slot AlgorithmWriteReadlooploopb-3: Rp = Ia-2: Wp=!ra-1: Wi = ! Li[ Wp ]b-2: r = RpCells [ Wp ] [Wi] = valueb-1: Ri= Li[ Rp ]a.b: y=Cells [Rp ] [Ri]a+1: Li[Wp ] = Wia+2: I= Wp
Simpson 4 Slot Algorithm Write Read loop loop a-2: Wp = ! r b-3: Rp = l a-1: Wi = ! Li [ Wp ] b-2: r = Rp a: Cells [ Wp ] [ Wi ] = value b-1: Ri = Li [ Rp ] a+1: Li [ Wp ] = Wi b: y=Cells [ Rp ] [Ri ] a+2: l = Wp
Recent Work on VerifyingRegister AlgorithmsSeparation Logic. Quite complicated
Recent Work on Verifying Register Algorithms Separation Logic. Quite complicated