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 propo...

Full description

Saved in:
Bibliographic Details
Main Authors: El-kustaban, A., Moszkowski, B., Cau, A.
Format: Conference Proceeding
Language:English
Subjects:
Abstracts
Cognition
Computational modeling
History
Safety
Semantics
Software
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
DOI:10.1109/SCET.2012.6342060