Zobrazeno 1 - 10
of 170
pro vyhledávání: '"Donaldson, Alastair"'
We report our experience formally modelling and verifying CXL.cache, the inter-device cache coherence protocol of the Compute Express Link standard. We have used the Isabelle proof assistant to create a formal model for CXL.cache based on the prose E
Externí odkaz:
http://arxiv.org/abs/2410.15908
Autor:
Geeson, Luke, Brotherston, James, Dijkstra, Wilco, Donaldson, Alastair F., Smith, Lee, Sorensen, Tyler, Wickerson, John
The correctness of complex software depends on the correctness of both the source code and the compilers that generate corresponding binary code. Compilers must do more than preserve the semantics of a single source file: they must ensure that genera
Externí odkaz:
http://arxiv.org/abs/2409.01161
Memory persistency models provide a foundation for persistent programming by specifying which (and when) writes to non-volatile memory (NVM) become persistent. Memory persistency models for the Intel-x86 and Arm architectures have been formalised, bu
Externí odkaz:
http://arxiv.org/abs/2405.18575
We present a method for systematically evaluating the correctness and robustness of instruction-tuned large language models (LLMs) for code generation via a new benchmark, Turbulence. Turbulence consists of a large set of natural language $\textit{qu
Externí odkaz:
http://arxiv.org/abs/2312.14856
Autor:
Sorensen, Tyler, Salvador, Lucas F., Raval, Harmit, Evrard, Hugues, Wickerson, John, Martonosi, Margaret, Donaldson, Alastair F.
As GPU availability has increased and programming support has matured, a wider variety of applications are being ported to these platforms. Many parallel applications contain fine-grained synchronization idioms; as such, their correct execution depen
Externí odkaz:
http://arxiv.org/abs/2109.06132
Autor:
Donaldson, Alastair F.
This is a report on the PLDI 2020 conference, for which I was General Chair, which was held virtually for the first time as a result of the COVID-19 pandemic. The report contains: my personal reflections on the positive and negative aspects of the ev
Externí odkaz:
http://arxiv.org/abs/2007.11686
Publikováno v:
Proceedings of the ACM on Programming Languages, 2019
Despite much recent interest in compiler randomized testing (fuzzing), the practical impact of fuzzer-found compiler bugs on real-world applications has barely been assessed. We present the first quantitative and qualitative study of the tangible imp
Externí odkaz:
http://arxiv.org/abs/1902.09334
Multi-core architectures can be leveraged to allow independent processes to run in parallel. However, due to resources shared across cores, such as caches, distinct processes may interfere with one another, e.g. affecting execution time. Analysing th
Externí odkaz:
http://arxiv.org/abs/1809.05197
There is growing interest in accelerating irregular data-parallel algorithms on GPUs. These algorithms are typically blocking, so they require fair scheduling. But GPU programming models (e.g.\ OpenCL) do not mandate fair scheduling, and GPU schedule
Externí odkaz:
http://arxiv.org/abs/1707.01989
The discovery of inductive invariants lies at the heart of static program verification. Presently, many automatic solutions to inductive invariant generation are inflexible, only applicable to certain classes of programs, or unpredictable. An automat
Externí odkaz:
http://arxiv.org/abs/1612.01198