Sangam: A Confluence of Knowledge Streams

Studying and Analysing Transactional Memory Using Interval Temporal Logic and AnaTempura

Show simple item record

dc.creator El-kustaban, Amin Mohammed Ahmed
dc.date 2012-08-22T13:34:52Z
dc.date 2012-08-22T13:34:52Z
dc.date 2012
dc.date.accessioned 2023-02-22T17:04:38Z
dc.date.available 2023-02-22T17:04:38Z
dc.identifier http://hdl.handle.net/2086/6900
dc.identifier.uri http://localhost:8080/xmlui/handle/CUHPOERS/254441
dc.description 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.
dc.format application/pdf
dc.language en
dc.publisher De Montfort University
dc.publisher Faculty of Technology
dc.publisher Software Technology Research Laboratory
dc.subject transactional memory
dc.subject Interval Temporal Logic
dc.subject AnaTempura
dc.subject Formal Verification of Transactional Memory
dc.title Studying and Analysing Transactional Memory Using Interval Temporal Logic and AnaTempura
dc.type Thesis or dissertation
dc.type Doctoral
dc.type PhD


Files in this item

Files Size Format View
Amin El-kustaban's Thesis.pdf 5.605Mb application/pdf View/Open

This item appears in the following Collection(s)

Show simple item record

Search DSpace


Advanced Search

Browse