Proving the correctness of optimising destructive and non-destructive reads over tuple spacess

 Rocco De Nicola1, Rosario Pugliese1, Antony Rowstron2,
1 Dipartimento di Sistemi e Informatica, Universita' di Firenze, Via C. Lombroso 6/17, Firenze
2 Microsoft Research Ltd, St. George House, 1 Guildhall Street, Cambridge

Abstract
In this paper we describe the proof of an optimisation that can be applied to tuple space based run-time systems (as used in Linda). The optimisation allows, under certain circumstances, for a tuple that has been destructively removed from a shared tuple space (for example, by a Linda in) to be returned as the result for a non-destructive read (for example, a Linda rd) for a different process. The optimisation has been successfully used in a prototype run-time system.