אירועים והרצאות בפקולטה למדעי המחשב ע"ש הנרי ומרילין טאוב

Transactional memory (TM) eases the task of writing concurrent applications by letting the programmer designate certain code blocks as atomic. One of the main challenges in stating the correctness of TM systems is the need to provide guarantees on the system state observed by live transactions. While several consistency conditions have been suggested for TM, they fall short of formalizing the intuitive semantics of atomic blocks. A TM consistency condition should be weak enough to allow flexibility in implementation, yet strong enough to disallow undesirable TM behavior, which can lead to run-time errors in live transactions. The latter feature is formalized by observational refinement between TM implementations, stating that properties of a program using a concrete TM mplementation can be established by analyzing its behavior with an abstract TM. We show that Strong Transactional Memory Specification (STMS), a variant of Transactional Memory Specification (TMS), a TM correctness condition, is necessary and sufficient for observational refinement for a programming language in which local variables are not rolled back upon an abort. We also show that TMS is necessary and sufficient for observational refinement for the common programming model in which local variables are rolled back upon a transaction abort. This makes STMS and TMS the weakest acceptable conditions for these programming models. We show that STMS is prefix-closed and under certain restrictions, limit-closed Therefore, STMS is a safety property, and to prove that a TM implementation is STMS, it suffices to prove that all its finite histories are STMS. We also show that STMS is weaker than Opacity, a well-known consistency condition, and under certain restrictions, STMS is equivalent to Opacity.