Timing properties and correctness for structured parallel programs on x86-64 multicores

Kevin Hammond; Christopher Mark Brown; Susmit Sarkar

doi:10.1007/978-3-319-46559-3_6

Timing properties and correctness for structured parallel programs on x86-64 multicores

Kevin Hammond, Christopher Mark Brown, Susmit Sarkar

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

This paper determines correctness and timing properties for structured parallel programs on x86-64 multicores. Multicore architectures are increasingly common, but real architectures have unpredictable timing properties, and even
correctness is not obvious above the relaxed-memory concurrency models
that are enforced by commonly-used hardware. This paper takes a rigorous approach to correctness and timing properties, examining common locking protocols from first principles, and extending this through queues to structured parallel constructs. We prove functional correctness and derive simple timing models, and both extend for the first time from low-level primitives to high-level parallel patterns. Our derived high-level timing models for structured parallel programs allow us to accurately predict upper bounds on program
execution times on x86-64 multicores.

Original language	English
Title of host publication	Foundational and Practical Aspects of Resource Analysis
Subtitle of host publication	4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers
Editors	Marko van Eekelen, Ugo Dal Lago
Publisher	Springer
Pages	101-125
Number of pages	26
ISBN (Electronic)	9783319465593
ISBN (Print)	9783319465586
DOIs	https://doi.org/10.1007/978-3-319-46559-3_6
Publication status	Published - 2016
Event	4th International Workshop, Foundational and Practical Aspects of Resource Analysis (FOPARA 2015) - London, United Kingdom Duration: 11 Apr 2015 → 11 Apr 2015 Conference number: 4 http://resourceanalysis.cs.ru.nl/fopara/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9964
ISSN (Print)	0302-9743

Workshop

Workshop	4th International Workshop, Foundational and Practical Aspects of Resource Analysis (FOPARA 2015)
Abbreviated title	FOPARA
Country/Territory	United Kingdom
City	London
Period	11/04/15 → 11/04/15
Internet address	http://resourceanalysis.cs.ru.nl/fopara/

Keywords

Multicore
Relaxed-memory concurrency
Functional correctness
Algorithmic skeletons
Operational semantics
Timing models

Access to Document

10.1007/978-3-319-46559-3_6

fopara
© 2016, Springer International Switzerland. This work has been made available online in accordance with the publisher’s policies. This is the author created, accepted version manuscript following peer review and may differ slightly from the final published version. The final published version of this work is available at link.springer.com / https://doi.org/ 10.1007/978-3-319-46559-3 6
Accepted author manuscript, 712 KBLicence: Unspecified

H2020 Collaboration REPHRASE: H2020 Collaboration 2014 - RePhrase
Hammond, K. (PI)
European Commission
1/04/15 → 31/03/18
Project: Standard

Timing Properties and Correctness for Structured Parallel Programs on x86-64 Multicores - Dataset
Hammond, K. (Creator), Brown, C. M. (Creator) & Sarkar, S. (Creator), Zenodo, 19 Jul 2016
DOI: 10.5281/zenodo.58198
Dataset

Cite this

Hammond, K., Brown, C. M., & Sarkar, S. (2016). Timing properties and correctness for structured parallel programs on x86-64 multicores. In M. van Eekelen, & U. Dal Lago (Eds.), Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers (pp. 101-125). (Lecture Notes in Computer Science; Vol. 9964). Springer. https://doi.org/10.1007/978-3-319-46559-3_6

Hammond, Kevin ; Brown, Christopher Mark ; Sarkar, Susmit. / Timing properties and correctness for structured parallel programs on x86-64 multicores. Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers. editor / Marko van Eekelen ; Ugo Dal Lago. Springer, 2016. pp. 101-125 (Lecture Notes in Computer Science).

@inproceedings{6e70a1deb0e544e1a7885ceb09100b7f,

title = "Timing properties and correctness for structured parallel programs on x86-64 multicores",

abstract = "This paper determines correctness and timing properties for structured parallel programs on x86-64 multicores. Multicore architectures are increasingly common, but real architectures have unpredictable timing properties, and evencorrectness is not obvious above the relaxed-memory concurrency modelsthat are enforced by commonly-used hardware. This paper takes a rigorous approach to correctness and timing properties, examining common locking protocols from first principles, and extending this through queues to structured parallel constructs. We prove functional correctness and derive simple timing models, and both extend for the first time from low-level primitives to high-level parallel patterns. Our derived high-level timing models for structured parallel programs allow us to accurately predict upper bounds on programexecution times on x86-64 multicores.",

keywords = "Multicore, Relaxed-memory concurrency, Functional correctness, Algorithmic skeletons, Operational semantics, Timing models",

author = "Kevin Hammond and Brown, {Christopher Mark} and Susmit Sarkar",

year = "2016",

doi = "10.1007/978-3-319-46559-3_6",

language = "English",

isbn = "9783319465586",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "101--125",

editor = "{van Eekelen}, Marko and {Dal Lago}, Ugo",

booktitle = "Foundational and Practical Aspects of Resource Analysis",

address = "Netherlands",

note = "4th International Workshop, Foundational and Practical Aspects of Resource Analysis (FOPARA 2015), FOPARA ; Conference date: 11-04-2015 Through 11-04-2015",

url = "http://resourceanalysis.cs.ru.nl/fopara/",

}

Hammond, K, Brown, CM & Sarkar, S 2016, Timing properties and correctness for structured parallel programs on x86-64 multicores. in M van Eekelen & U Dal Lago (eds), Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers. Lecture Notes in Computer Science, vol. 9964, Springer, pp. 101-125, 4th International Workshop, Foundational and Practical Aspects of Resource Analysis (FOPARA 2015), London, United Kingdom, 11/04/15. https://doi.org/10.1007/978-3-319-46559-3_6

Timing properties and correctness for structured parallel programs on x86-64 multicores. / Hammond, Kevin; Brown, Christopher Mark ; Sarkar, Susmit.
Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers. ed. / Marko van Eekelen; Ugo Dal Lago. Springer, 2016. p. 101-125 (Lecture Notes in Computer Science; Vol. 9964).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Timing properties and correctness for structured parallel programs on x86-64 multicores

AU - Hammond, Kevin

AU - Brown, Christopher Mark

AU - Sarkar, Susmit

N1 - Conference code: 4

PY - 2016

Y1 - 2016

N2 - This paper determines correctness and timing properties for structured parallel programs on x86-64 multicores. Multicore architectures are increasingly common, but real architectures have unpredictable timing properties, and evencorrectness is not obvious above the relaxed-memory concurrency modelsthat are enforced by commonly-used hardware. This paper takes a rigorous approach to correctness and timing properties, examining common locking protocols from first principles, and extending this through queues to structured parallel constructs. We prove functional correctness and derive simple timing models, and both extend for the first time from low-level primitives to high-level parallel patterns. Our derived high-level timing models for structured parallel programs allow us to accurately predict upper bounds on programexecution times on x86-64 multicores.

AB - This paper determines correctness and timing properties for structured parallel programs on x86-64 multicores. Multicore architectures are increasingly common, but real architectures have unpredictable timing properties, and evencorrectness is not obvious above the relaxed-memory concurrency modelsthat are enforced by commonly-used hardware. This paper takes a rigorous approach to correctness and timing properties, examining common locking protocols from first principles, and extending this through queues to structured parallel constructs. We prove functional correctness and derive simple timing models, and both extend for the first time from low-level primitives to high-level parallel patterns. Our derived high-level timing models for structured parallel programs allow us to accurately predict upper bounds on programexecution times on x86-64 multicores.

KW - Multicore

KW - Relaxed-memory concurrency

KW - Functional correctness

KW - Algorithmic skeletons

KW - Operational semantics

KW - Timing models

U2 - 10.1007/978-3-319-46559-3_6

DO - 10.1007/978-3-319-46559-3_6

M3 - Conference contribution

SN - 9783319465586

T3 - Lecture Notes in Computer Science

SP - 101

EP - 125

BT - Foundational and Practical Aspects of Resource Analysis

A2 - van Eekelen, Marko

A2 - Dal Lago, Ugo

PB - Springer

T2 - 4th International Workshop, Foundational and Practical Aspects of Resource Analysis (FOPARA 2015)

Y2 - 11 April 2015 through 11 April 2015

ER -

Hammond K, Brown CM , Sarkar S. Timing properties and correctness for structured parallel programs on x86-64 multicores. In van Eekelen M, Dal Lago U, editors, Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers. Springer. 2016. p. 101-125. (Lecture Notes in Computer Science). Epub 2016 Sept 25. doi: 10.1007/978-3-319-46559-3_6

Timing properties and correctness for structured parallel programs on x86-64 multicores

Abstract

Publication series

Workshop

Keywords

Access to Document

Fingerprint

Projects

H2020 Collaboration REPHRASE: H2020 Collaboration 2014 - RePhrase

Datasets

Timing Properties and Correctness for Structured Parallel Programs on x86-64 Multicores - Dataset

Cite this