Výsledky vyhledávání

ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS

Autor: Christopher Pulte, Robert M. Norton, Ian Stark, Jon French, Alastair Reid, Shaked Flur, Alasdair Armstrong, Mark Wassell, Kathryn E. Gray, Peter Sewell, Neel Krishnaswami, Thomas Bauereiss, Brian Campbell, Prashanth Mundkur

Publikováno v: Proceedings of the ACM on Programming Languages
Armstrong, A, Bauereiss, T, Campbell, B, Reid, A, Gray, K E, Norton, R M, Mundkur, P, Wassell, M, French, J, Pulte, C, Flur, S, Stark, I, Krishnaswami, N & Sewell, P 2019, ' ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS ', Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, 71 . https://doi.org/10.1145/3290384

Architecture specifications notionally define the fundamental interface between hardware and software: the envelope of allowed behaviour for processor implementations, and the basic assumptions for software development and verification. But in practi

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b03d45b0127eedfeee57ea420de43824
https://doi.org/10.1145/3290384

Zobrazit plný text záznamu

ARMv8-A system semantics: instruction fetch in relaxed architectures

Autor: Christopher Pulte, Alasdair Armstrong, Peter Sewell, Luc Maranget, Jean Pichon-Pharabod, Shaked Flur, Ben Simner

Publikováno v: ESOP 2020-29th European Symposium on Programming
ESOP 2020-29th European Symposium on Programming, Mar 2020, Dublin, Ireland
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Programming Languages and Systems
Programming Languages and Systems ISBN: 9783030449131
ESOP
Programming Languages and Systems-29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings
Programming Languages and Systems

Computing relies on architecture specifications to decouple hardware and software development. Historically these have been prose documents, with all the problems that entails, but research over the last ten years has developed rigorous and executabl

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6381fb55d3b77293ae2261bf3ddf52a2
https://hal.inria.fr/hal-02509910/file/esop2020.pdf

Zobrazit plný text záznamu

Repairing and mechanising the JavaScript relaxed memory model

Autor: Anton Podkopaev, Christopher Pulte, Guillaume Barbier, Jean Pichon-Pharabod, Shaked Flur, Conrad Watt, Shu-yu Guo, Stephen K. Dolan

Publikováno v: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
PLDI

Modern JavaScript includes the SharedArrayBuffer feature, which provides access to true shared memory concurrency. SharedArrayBuffers are simple linear buffers of bytes, and the JavaScript specification defines an axiomatic relaxed memory model to de

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::fe4d3ef82ef5ee8ff0d263f9f5db1dc7

Zobrazit plný text záznamu

Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8

Autor: Christopher Pulte, Shaked Flur, Peter Sewell, Will Deacon, Susmit Sarkar, Jon French

Publikováno v: Proceedings of the ACM on Programming Languages. 2:1-29

ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8. Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e0e74f5947fa0fafc570661ceac2fd33
https://doi.org/10.1145/3158107

Zobrazit plný text záznamu

Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC

Autor: Susmit Sarkar, Peter Sewell, Mark Batty, Christopher Pulte, Kyndylan Nienhuis, Ali Sezgin, Luc Maranget, Shaked Flur, Kathryn E. Gray

Publikováno v: 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017)
44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), ACM, Jan 2017, Paris, France
POPL

This work was partly funded by the EPSRC Programme Grant REMS: Rigorous Engineering for Mainstream Systems, EP/K008528/1, EPSRC grant C3: Scalable & Verified Shared Memory via Consistency-directed Cache Coherence EP/M027317/1 (Sarkar), an ARM iCASE a

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::28e5ffb005cc51cf5dd097d1971c6ded
https://kar.kent.ac.uk/64723/1/mixed-size.pdf

Zobrazit plný text záznamu

Termination proofs for linear simple loops

Autor: Supratik Mukhopadhyay, Hong Yi Chen, Shaked Flur

Publikováno v: International Journal on Software Tools for Technology Transfer. 17:47-57

Analysis of termination and other liveness properties of a program can be reduced to termination proof synthesis for simple loops, i.e., loops with only variable updates in the loop body. Among simple loops, the subset of linear simple loops (LSLs) i

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::183c252348bb541fabdaddb2ce83acec
https://doi.org/10.1007/s10009-013-0288-8

Zobrazit plný text záznamu

Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA

Autor: Kathryn E. Gray, Christopher Pulte, Ali Sezgin, Peter Sewell, Luc Maranget, Will Deacon, Susmit Sarkar, Shaked Flur

Publikováno v: Principles of Programming Languages 2016 (POPL 2016)
Principles of Programming Languages 2016 (POPL 2016), Jan 2016, Saint Petersburg, United States
POPL

This work was partly funded by the EPSRC Programme Grant REMS: Rigorous Engineering for Mainstream Systems, EP/K008528/1, the Scottish Funding Council (SICSA Early Career Industry Fellowship, Sarkar), an ARM iCASE award (Pulte), and ANR grant WMC (AN

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3ff47d827ee18455402b0595f5a65e4c
https://hal.inria.fr/hal-01244776

Zobrazit plný text záznamu

Termination Proofs for Linear Simple Loops

Autor: Supratik Mukhopadhyay, Hong Yi Chen, Shaked Flur

Publikováno v: Static Analysis ISBN: 9783642331244
SAS

Analysis of termination and other liveness properties of an imperative program can be reduced to termination proof synthesis for simple loops, i.e., loops with only variable updates in the loop body. Among simple loops, the subset of Linear Simple Lo

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::0e4ea0475c363875b27dab5ef5b4d2b6
https://doi.org/10.1007/978-3-642-33125-1_28

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání