uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Caches, Transactions and Memories: Models, Coherence and Consistency
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
2018 (English)Doctoral thesis, comprehensive summary (Other academic)
Description
Abstract [en]

Computers have brought us inestimable convenience in recent years. We have become dependent on them and more sensitive to their performance. During the past decades, we have been trying to improve program efficiency. The invention of multi-core systems is regarded as the new era of boosting performance of computer programs. When we focus on improving program efficiency, we also need to pay attention to program correctness. In some specific areas, errors, aka bugs, of programs can cause disastrous consequences. The dominant approach to bug detection is testing, which is conducted by executing a program against test cases generated based on scenarios. A bug is found when the output of the program does not match the expected output defined in the test case. One main drawback of testing is that it only shows the presence of bugs. An alternative approach is formal verification, which is a method that can exhaustively analyze the program executions and therefore show the absence of bugs. This thesis focuses on one of the main areas of formal verification - model checking. Model checking analyzes a mathematical model extracted from a program and automatically checks if it satisfies the desired properties.

In this thesis, we first consider verifying safety and liveness properties for transactional memories. In particular, we consider the FlexTM hybrid transactional memory. We build a formal model of FlexTM, and apply a small model theorem that restricts the number of threads and variables in the model. This allows us to reduce the problem of verifying safety and liveness properties of FlexTM to checking language inclusion between the automata of FlexTM and a reference transactional memory. Second, we present a method for automatic verification of cache coherence protocols in the presence of transactional memories. We build a formal model containing a filter that represents the conflict resolution strategies of the transactional memory. We also apply a small model theorem which limits the number of cache lines of the protocol. To check cache coherence, we extend a backward reachability algorithm for infinite state systems, by removing the traces not allowed by the filter. Using this technique, we verify two cache protocols under different transactional memories respectively and conclude that they both maintain coherence.  Finally, we consider verification of safety properties of programs running over Self-Invalidate and Self-Downgrade cache coherence protocols. To that end, we define a formal model which captures the weak memory model induced by such protocols. We design an algorithm for inserting a set of optimal fences in the program, which guarantees the safety property while still maintaining the efficiency of a maximal degree.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2018. , p. 83
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1665
Keywords [en]
cache coherence protocol, transactional memory, weak memory model, model checking, parameterized system
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-347787ISBN: 978-91-513-0321-5 (print)OAI: oai:DiVA.org:uu-347787DiVA, id: diva2:1196319
Public defence
2018-05-30, ITC/2446, Lägerhyddsvägen 2, Uppsala, 09:00 (English)
Opponent
Supervisors
Available from: 2018-05-08 Created: 2018-04-09 Last updated: 2018-05-08
List of papers
1. Verifying safety and liveness for the FlexTM hybrid transactional memory
Open this publication in new window or tab >>Verifying safety and liveness for the FlexTM hybrid transactional memory
Show others...
2013 (English)Conference paper, Published paper (Refereed)
Abstract [en]

We consider the verification of safety (strict serializability and abort consistency) and liveness obstruction and livelock freedom) for the hybrid transactional memory framework FlexTM. This framework allows for flexible implementations of transactional memories based on an adaptation of the MESI coherence protocol. FlexTM allows for both eager and lazy conflict resolution strategies. Like in the case of Software Transactional Memories, the verification problem is not trivial as the number of concurrent transactions, their size, and the number of accessed shared variables cannot be a priori bounded. This complexity is exacerbated by aspects that are specific to hardware and hybrid transactional memories. Our work takes into account intricate behaviours such as cache line based conflict detection, false sharing, invisible reads or non-transactional instructions. We carry out the first automatic verification of a hybrid transactional memory and establish, by adopting a small model approach, challenging properties such as strict serializability, abort consistency, and obstruction freedom for both an eager and a lazy conflict resolution strategies. We also detect an example that refutes livelock freedom. To achieve this, our prototype tool makes use of the latest antichain based techniques to handle systems with tens of thousands of states.

Place, publisher, year, edition, pages
Grenoble, France: , 2013
National Category
Computer Systems
Identifiers
urn:nbn:se:uu:diva-213232 (URN)978-1-4503-2153-2 (ISBN)
Conference
Design, Automation and Test in Europe, DATE 13, Grenoble, France, March 18-22, 2013
Projects
UPMARC
Available from: 2013-12-19 Created: 2013-12-19 Last updated: 2018-04-09
2. Verification of Cache Coherence Protocols wrt. Trace Filters
Open this publication in new window or tab >>Verification of Cache Coherence Protocols wrt. Trace Filters
Show others...
2015 (English)In: Proc. 15th Conference on Formal Methods in Computer-Aided Design, Piscataway, NJ: IEEE , 2015, p. 9-16Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Piscataway, NJ: IEEE, 2015
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-272322 (URN)978-0-9835678-5-1 (ISBN)
Conference
FMCAD 2015, September 27–30, Austin, TX
Projects
UPMARC
Available from: 2015-09-30 Created: 2016-01-13 Last updated: 2018-04-09
3. Fencing programs with self-invalidation and self-downgrade
Open this publication in new window or tab >>Fencing programs with self-invalidation and self-downgrade
Show others...
2016 (English)In: Formal Techniques for Distributed Objects, Components, and Systems, Springer, 2016, p. 19-35Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer, 2016
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9688
National Category
Computer Engineering
Identifiers
urn:nbn:se:uu:diva-300663 (URN)10.1007/978-3-319-39570-8_2 (DOI)000379297600002 ()978-3-319-39569-2 (ISBN)
Conference
FORTE 2016, June 6–9, Heraklion, Greece
Projects
UPMARC
Available from: 2016-05-24 Created: 2016-08-10 Last updated: 2018-04-09Bibliographically approved
4. Mending fences with self-invalidation and self-downgrade
Open this publication in new window or tab >>Mending fences with self-invalidation and self-downgrade
Show others...
2018 (English)In: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 14, no 1, article id 6Article in journal (Refereed) Published
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-347675 (URN)000426512000004 ()
Available from: 2018-01-16 Created: 2018-04-06 Last updated: 2018-05-17Bibliographically approved

Open Access in DiVA

fulltext(1181 kB)36 downloads
File information
File name FULLTEXT01.pdfFile size 1181 kBChecksum SHA-512
d3de7e5078befbd43df105403cb57a3a6789cc7bbc067451df853f7b3ab528c8c4360b4bae57e3a95604a6de877ef2180e5b8f0cd5f71ddb627b0c5731e5d748
Type fulltextMimetype application/pdf

Authority records BETA

Zhu, Yunyun

Search in DiVA

By author/editor
Zhu, Yunyun
By organisation
Computer SystemsDivision of Computer Systems
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 36 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 408 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf