kirancodes.me
To Proof Maintenance & Beyond!

Practical concurrent traversals in search trees

Dana Drachsler-Cohen, Martin T. Vechev, Eran Yahav

Abstract

Operations of concurrent objects often employ optimistic concurrency-control schemes that consist of a traversal followed by a validation step. The validation checks if concurrent mutations interfered with the traversal to determine if the operation should proceed or restart. A fundamental challenge is to discover a necessary and sufficient validation check that has to be performed to guarantee correctness.

Related papers