Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Fencing programs with self-invalidation and self-downgrade
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation.
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
Visa övriga samt affilieringar
2016 (Engelska)Ingår i: Formal Techniques for Distributed Objects, Components, and Systems, Springer, 2016, s. 19-35Konferensbidrag, Publicerat paper (Refereegranskat)
Resurstyp
Text
Ort, förlag, år, upplaga, sidor
Springer, 2016. s. 19-35
Serie
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9688
Nationell ämneskategori
Datorteknik
Identifikatorer
URN: urn:nbn:se:uu:diva-300663DOI: 10.1007/978-3-319-39570-8_2ISI: 000379297600002ISBN: 978-3-319-39569-2 (tryckt)OAI: oai:DiVA.org:uu-300663DiVA, id: diva2:951820
Konferens
FORTE 2016, June 6–9, Heraklion, Greece
Projekt
UPMARCTillgänglig från: 2016-05-24 Skapad: 2016-08-10 Senast uppdaterad: 2018-04-09Bibliografiskt granskad
Ingår i avhandling
1. Caches, Transactions and Memories: Models, Coherence and Consistency
Öppna denna publikation i ny flik eller fönster >>Caches, Transactions and Memories: Models, Coherence and Consistency
2018 (Engelska)Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
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.

Ort, förlag, år, upplaga, sidor
Uppsala: Acta Universitatis Upsaliensis, 2018. s. 83
Serie
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1665
Nyckelord
cache coherence protocol, transactional memory, weak memory model, model checking, parameterized system
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
Datavetenskap
Identifikatorer
urn:nbn:se:uu:diva-347787 (URN)978-91-513-0321-5 (ISBN)
Disputation
2018-05-30, ITC/2446, Lägerhyddsvägen 2, Uppsala, 09:00 (Engelska)
Opponent
Handledare
Tillgänglig från: 2018-05-08 Skapad: 2018-04-09 Senast uppdaterad: 2018-05-08

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltext

Sök vidare i DiVA

Av författaren/redaktören
Abdulla, Parosh AzizAtig, Mohamed FaouziKaxiras, StefanosLeonardsson, CarlRos, AlbertoZhu, Yunyun
Av organisationen
DatorteknikDatorarkitektur och datorkommunikation
Datorteknik

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetricpoäng

doi
isbn
urn-nbn
Totalt: 412 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf