{"id":{"repo_id":"de-montfort","oai_identifier":"oai:dora.dmu.ac.uk:2086/6900"},"canonical_url":"https://search.dev.ndltd.org/etd/de-montfort/oai:dora.dmu.ac.uk:2086/6900","repository":{"repo_id":"de-montfort","name":"De Montfort University","base_url":"https://dora.dmu.ac.uk/server/oai/request"},"display":{"title":"Studying and Analysing Transactional Memory Using Interval Temporal Logic and AnaTempura","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.","abstract_html":"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.","abstract_has_math":false,"creators":["El-kustaban, Amin Mohammed Ahmed"],"institution":"De Montfort University","degree_name":"PhD","degree_level":"Doctoral","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2012,"date_issued":"2012","date_published":"2012","updated_at":"2026-07-24T06:18:24Z","subjects":["transactional memory","Interval Temporal Logic","AnaTempura","Formal Verification of Transactional Memory"],"languages":[],"rights":[],"rights_urls":["https://dora.dmu.ac.uk/bitstreams/b6c17da6-4683-44ce-855d-7c1e8ddcec0f/download"],"identifier_entries":[]},"links":{"outbound_url":null,"outbound_label":null,"outbound_source":null},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["El-kustaban, Amin Mohammed Ahmed"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.issued","label":"Date","values":["2012"]},{"key":"dc:publisher.department","label":"Dc Publisher Department","values":["Faculty of Technology","Software Technology Research Laboratory"]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["De Montfort University"]},{"key":"dc:relation.isreferencedby","label":"Dc Relation Isreferencedby","values":["http://hdl.handle.net/2086/6900"]},{"key":"dc:type","label":"Dc Type","values":["Thesis or dissertation"]},{"key":"dc:type.qualificationlevel","label":"Dc Type Qualificationlevel","values":["Doctoral"]},{"key":"dc:type.qualificationname","label":"Dc Type Qualificationname","values":["PhD"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["transactional memory","Interval Temporal Logic","AnaTempura","Formal Verification of Transactional Memory"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:rights","label":"Dc Rights","values":["https://dora.dmu.ac.uk/bitstreams/b6c17da6-4683-44ce-855d-7c1e8ddcec0f/download"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://dora.dmu.ac.uk/bitstreams/19502f4b-c384-47fe-929e-1daa7f04f613/download"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:format.checksum.md5","label":"Dc Format Checksum Md5","values":["dbf36a9c501da2778d9bc20c128c0a8f","0fc94b8b5788858195354ebb68baf968","497d4be73d40d32a635169399f31b7e9"]},{"key":"dc:title","label":"Title","values":["Studying and Analysing Transactional Memory Using Interval Temporal Logic and AnaTempura"]}]}],"canonical_facts":{"dc:creator":["El-kustaban, Amin Mohammed Ahmed"],"dc:date.issued":["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."],"dc:format.checksum.md5":["dbf36a9c501da2778d9bc20c128c0a8f","0fc94b8b5788858195354ebb68baf968","497d4be73d40d32a635169399f31b7e9"],"dc:identifier.uri":["https://dora.dmu.ac.uk/bitstreams/19502f4b-c384-47fe-929e-1daa7f04f613/download"],"dc:publisher.department":["Faculty of Technology","Software Technology Research Laboratory"],"dc:publisher.institution":["De Montfort University"],"dc:relation.isreferencedby":["http://hdl.handle.net/2086/6900"],"dc:rights":["https://dora.dmu.ac.uk/bitstreams/b6c17da6-4683-44ce-855d-7c1e8ddcec0f/download"],"dc:subject":["transactional memory","Interval Temporal Logic","AnaTempura","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.qualificationlevel":["Doctoral"],"dc:type.qualificationname":["PhD"]},"updated_at":"2026-07-24T06:18:24Z"}