Studying and Analysing Transactional Memory Using Interval Temporal Logic and AnaTempura

De Montfort University Open Research Archive

Show simple item record El-kustaban, Amin Mohammed Ahmed 2012-08-22T13:34:52Z 2012-08-22T13:34:52Z 2012
dc.description.abstract Transactional memory (TM) is a promising lock-free synchronisation technique which offers a high-level abstract parallel programming model for future chip multiprocessor (CMP) systems. Moreover, it adapts the well-established popular paradigm of transactions and thus provides a general and flexible way to allow programs to read and modify disparate memory locations atomically as a single operation. In this thesis, we propose a general framework for validating a TM design, starting from a formal specification into a hardware implementation, with its underpinning theory and refinement. A methodology in this work starts with a high-level and executable specification model for an abstract TM with verification for various correctness conditions of concurrent transactions. This model is constructed within a flexible transition framework that allows verifying correctness of a TM system with animation. Then, we present a formal executable specification for a chip-dual single-cycle MIPS processor with a cache coherence protocol and integrate the provable TM system. Finally, we transform the dual processors with the TM from a high-level description into a Hardware Description Language (VHDL), using some proposed refinement and restriction rules. Interval Temporal Logic (ITL) and its programming language subset AnaTempura are used to build, execute and test the model, since they together provide a powerful framework supporting logical reasoning about time intervals as well as programming and simulation. en
dc.language.iso en en
dc.publisher De Montfort University en
dc.subject transactional memory en
dc.subject Interval Temporal Logic en
dc.subject AnaTempura en
dc.subject Formal Verification of Transactional Memory en
dc.title Studying and Analysing Transactional Memory Using Interval Temporal Logic and AnaTempura en
dc.type Thesis or dissertation en
dc.publisher.department Faculty of Technology en
dc.publisher.department Software Technology Research Laboratory en
dc.type.qualificationlevel Doctoral en
dc.type.qualificationname PhD en

Files in this item

This item appears in the following Collection(s)

Show simple item record