Show simple item record

dc.contributor.authorEl-kustaban, Amin Mohammed Ahmed
dc.date.accessioned2012-08-22T13:34:52Z
dc.date.available2012-08-22T13:34:52Z
dc.date.issued2012
dc.identifier.urihttp://hdl.handle.net/2086/6900
dc.description.abstractTransactional 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.isoenen
dc.publisherDe Montfort Universityen
dc.subjecttransactional memoryen
dc.subjectInterval Temporal Logicen
dc.subjectAnaTempuraen
dc.subjectFormal Verification of Transactional Memoryen
dc.titleStudying and Analysing Transactional Memory Using Interval Temporal Logic and AnaTempuraen
dc.typeThesis or dissertationen
dc.publisher.departmentFaculty of Technologyen
dc.publisher.departmentSoftware Technology Research Laboratoryen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhDen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record