Formalising of Transactional Memory Using Interval Temporal Logic (ITL)

Transactional memory (TM) is a promising lock-free technique that can avoid the problems associated with locking. It provides a more general and flexible way than other lock-based techniques by allowing programs to atomically read and modify disparate memory locations as a single operation. We propose a general specification model for an abstract TM with verification for various correctness conditions of concurrent transactions. This model has been constructed as a base to develop a general and flexible formal framework that can prove and validate the correctness of TM systems. Interval Temporal Logic (ITL) is used to build and verify this model, since it offers a powerful tool supporting logical reasoning about time intervals as well as programming and simulation.