Demonstration venue · read-only. Every page can be browsed; the buttons that would change it are switched off. Create an account to run TaxoReview on your own data. A simulation from public publication records: the people listed were not invited and did not agree to review.
? Tutorial for this page

Carl Leonardsson

dblp:58/11109 · DBLP profile ↗
← Back
11ranked-venue papers
0as first author
0since 2021 · last 2018
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 7Theory of computation · 3Systems, architecture and hardware · 2Computer networks · 1

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Software engineering, system software, and programming languages
2 papers
Concurrent programming · 73% Program verification · 27%
Computer architecture, parallel and distributed computing, and storage systems
1 paper
Memory systems · 100%

Topics — the 6 heaviest of 6, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Memory systems
cache coherence
0.312017
Efficient Self-Invalidation/Self-Downgrade for Critical Sections with Relaxed Semantics · IEEE Trans. Parallel Distributed Syst. 2017
Concurrent programming
concurrency verification
0.212016
Stateless Model Checking for POWER · CAV (2) 2016
Program verification › model checking
stateless model checking
0.212016
Stateless Model Checking for POWER · CAV (2) 2016
Concurrent programming › memory models
weak memory models
0.212016
Stateless Model Checking for POWER · CAV (2) 2016
Concurrent programming › synchronization
critical sections
0.112017
Efficient Self-Invalidation/Self-Downgrade for Critical Sections with Relaxed Semantics · IEEE Trans. Parallel Distributed Syst. 2017
Concurrent programming
synchronization
0.112017
Efficient Self-Invalidation/Self-Downgrade for Critical Sections with Relaxed Semantics · IEEE Trans. Parallel Distributed Syst. 2017

Methods — techniques the papers use, named apart from their topics

relaxed atomic operations · 0.6directory protocol · 0.6stateless model checking · 0.2
YearPublicationVenuePosition
2018 Mending Fences with Self-Invalidation and Self-Downgrade
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Stefanos Kaxiras, Carl Leonardsson, Alberto Ros 0001, Yunyun Zhu
Log. Methods Comput. Sci.4
2017 Stateless model checking for TSO and PSO
Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson 0001, Carl Leonardsson, Konstantinos Sagonas
Acta Informatica5
2017 Efficient Self-Invalidation/Self-Downgrade for Critical Sections with Relaxed Semantics
abstract
Cache coherence protocols based on self-invalidation allow simpler hardware implementation compared to traditional write-invalidation protocols, by relying on data-race-free semantics and applying self-invalidation on synchronization points. Their simplicity lies in the absence of invalidation traffic. This eliminates the need to track readers in a directory, and reduces the number of transient protocol states. Similarly, the use of self-downgrade on synchronization eliminates directory indirection, and hence the need to track writers in a directory. These protocols, effectively without a directory, have the potential to reduce area, energy consumption, and complexity, without sacrificing performance-provided, that self-invalidation and self-downgrade are performed prudently. In this work we examine how self-invalidation and self-downgrade are performed in relation to atomicity and ordering. We show that self-invalidation and self-downgrade do not need to be applied conservatively, as so far implemented. Our key observation is that, often, critical sections which are not ordered in time, are intended to provide only atomicity and not thread synchronization. We thus propose a new type of self-invalidation, forward-self-invalidation (FSI), which invalidates solely data that are going to be accessed inside a critical section. Based on the same reasoning, we propose a new type of self-downgrade, forward self-downgrade (FSD), also restricted to writes in critical sections. Finally, we define the semantics of locks using FSI and FSD, which resemble the semantics of relaxed atomic operations in C++. Our evaluation for 64-core multiprocessors shows significant improvements using the proposed FSI and FSD-where applicable-in Splash-3 and PARSEC benchmarks, over a directory-based protocol (17.1 percent in execution time and 33.9 percent in energy consumption) and also over a state-of-the-art self-invalidation/self-downgrade protocol (7.6 percent in execution time and 9.1 percent in energy consumption), while still retaining the design simplicity of the protocol.
Alberto Ros 0001, Carl Leonardsson, Christos Sakalis, Stefanos Kaxiras
IEEE Trans. Parallel Distributed Syst.2
2016 POSTER: Efficient Self-Invalidation/Self-Downgrade for Critical Sections with Relaxed Semantics
abstract
Cache coherence protocols based on self-invalidation allow simpler hardware implementation compared to traditional write-invalidation protocols, by relying on data-race-free semantics and applying self-invalidation and self-downgrade on synchronization points. This work examines how self-invalidation and self-downgrade are performed in relation to atomicity and ordering and shows that they do not need to be applied conservatively, as so far implemented. Our key observation is that, often, critical sections which are not ordered in time, are intended to provide only atomicity but not thread synchronization.
Alberto Ros 0001, Carl Leonardsson, Christos Sakalis, Stefanos Kaxiras
PACT2
2016 Stateless Model Checking for POWER
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson 0001, Carl Leonardsson
CAV (2)4
2016 Fencing Programs with Self-Invalidation and Self-Downgrade
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Stefanos Kaxiras, Carl Leonardsson, Alberto Ros 0001, Yunyun Zhu
FORTE4
2016 Splash-3: A properly synchronized benchmark suite for contemporary research
abstract
Benchmarks are indispensable in evaluating the performance implications of new research ideas. However, their usefulness is compromised if they do not work correctly on a system under evaluation or, in general, if they cannot be used consistently to compare different systems. A well-known benchmark suite of parallel applications is the Splash-2 suite. Since its creation in the context of the DASH project, Splash-2 benchmarks have been widely used in research. However, Splash-2 was released over two decades ago and does not adhere to the recent C memory consistency model. This leads to unexpected and often incorrect behavior when some Splash-2 benchmarks are used in conjunction with contemporary compilers and hardware (simulated or real). Most importantly, we discovered critical performance bugs that may question some of the reported benchmark results. In this work, we analyze the Splash-2 benchmarks and expose data races and related performance bugs. We rectify the problematic benchmarks and evaluate the resulting performance. Our work contributes to the community a new sanitized version of the Splash-2 benchmarks, called the Splash-3 benchmark suite.
Christos Sakalis, Carl Leonardsson, Stefanos Kaxiras, Alberto Ros 0001
ISPASS2
2015 Stateless Model Checking for TSO and PSO
Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson 0001, Carl Leonardsson, Konstantinos Sagonas
TACAS5
2013 Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen 0001, Carl Leonardsson, Ahmed Rezine
TACAS4
2012 Automatic Fence Insertion in Integer Programs via Predicate Abstraction
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen 0001, Carl Leonardsson, Ahmed Rezine
SAS4
2012 Counter-Example Guided Fence Insertion under TSO
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen 0001, Carl Leonardsson, Ahmed Rezine
TACAS4