John Wickerson

Proc. ACM Program. Lang., 2024

Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations.

[BibT_eX]

[DOI]

Luke Geeson

James Brotherston

Wilco Dijkstra

Lee Smith

Proc. ACM Program. Lang., 2024

Formalising CXL Cache Coherence.

[BibT_eX]

[DOI]

Chengsong Tan

CoRR, 2024

Lost in Interpretation: Navigating Challenges in Validating Persistency Models Amid Vague Specs and Stubborn Machines, All with a Sense of Humour.

[BibT_eX]

[DOI]

Vasileios Klimis

Viktor Vafeiadis

Azalea Raad

CoRR, 2024

Challenges in Empirically Testing Memory Persistency Models.

[BibT_eX]

[DOI]

Vasileios Klimis

Viktor Vafeiadis

Azalea Raad

Proceedings of the 2024 ACM/IEEE 44th International Conference on Software Engineering: New Ideas and Emerging Results, 2024

Automated Feature Testing of Verilog Parsers using Fuzzing (Registered Report).

[BibT_eX]

[DOI]

Quentin Corradi

Proceedings of the 3rd ACM International Fuzzing Workshop, 2024

Validating Database System Isolation Level Implementations with Version Certificate Recovery.

[BibT_eX]

[DOI]

Jack Clark

Manuel Rigger

Proceedings of the Nineteenth European Conference on Computer Systems, 2024

Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2024

Intel PMDK Transactions: Specification, Validation and Concurrency.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2024

2023

Simulating Operational Memory Models Using Off-the-Shelf Program Analysis Tools.

[BibT_eX]

[DOI]

Dan Iorga

IEEE Trans. Software Eng., December, 2023

Parallelising Control Flow in Dynamic-scheduling High-level Synthesis.

[BibT_eX]

[DOI]

ACM Trans. Reconfigurable Technol. Syst., December, 2023

Balancing Static Islands in Dynamically Scheduled Circuits Using Continuous Petri Nets.

[BibT_eX]

[DOI]

Estíbaliz Fraca

IEEE Trans. Computers, November, 2023

Taking Back Control in an Intermediate Representation for GPU Computing.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., January, 2023

Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2023

2022

A Case for Precise, Fine-Grained Pointer Synthesis in High-Level Synthesis.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2022

Optimal and Heuristic Approaches to Modulo Scheduling With Rational Initiation Intervals in Hardware Synthesis.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2022

DASS: Combining Dynamic & Static Scheduling in High-Level Synthesis.

[BibT_eX]

[DOI]

Paolo Ienne

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2022

Efficient Memory Arbitration in High-Level Synthesis From Multi-Threaded Code.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 2022

High-coverage metamorphic testing of concurrency support in C compilers.

[BibT_eX]

[DOI]

Matt Windsor

Softw. Test. Verification Reliab., 2022

View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2022

Dynamic Inter-Block Scheduling for HLS.

[BibT_eX]

[DOI]

Proceedings of the 32nd International Conference on Field-Programmable Logic and Applications, 2022

Finding and Finessing Static Islands in Dynamically Scheduled Circuits.

[BibT_eX]

[DOI]

Proceedings of the FPGA '22: The 2022 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays, Virtual Event, USA, 27 February 2022, 2022

Resource Sharing for Verified High-Level Synthesis.

[BibT_eX]

[DOI]

Michalis Pardalos

Yann Herklotz

Proceedings of the 30th IEEE Annual International Symposium on Field-Programmable Custom Computing Machines, 2022

Dynamic C-Slow Pipelining for HLS.

[BibT_eX]

[DOI]

Proceedings of the 30th IEEE Annual International Symposium on Field-Programmable Custom Computing Machines, 2022

View-Based Owicki-Gries Reasoning for Persistent x86-TSO.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2022

2021

Global Analysis of C Concurrency in High-Level Synthesis.

[BibT_eX]

[DOI]

IEEE Trans. Very Large Scale Integr. Syst., 2021

Specifying and testing GPU workgroup progress models.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

The semantics of shared memory in Intel CPU/FPGA systems.

[BibT_eX]

[DOI]

Dan Iorga

Proc. ACM Program. Lang., 2021

Formal verification of high-level synthesis.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

C4: the C compiler concurrency checker.

[BibT_eX]

[DOI]

Matt Windsor

Proceedings of the ISSTA '21: 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2021

Dreaming up Metamorphic Relations: Experiences from Three Fuzzer Tools.

[BibT_eX]

[DOI]

Andrei Lascu

Matt Windsor

Tobias Grosser

Proceedings of the 6th IEEE/ACM International Workshop on Metamorphic Testing, 2021

Exploiting the Correlation between Dependence Distance and Latency in Loop Pipelining for HLS.

[BibT_eX]

[DOI]

Proceedings of the 31st International Conference on Field-Programmable Logic and Applications, 2021

Fuzzing High-Level Synthesis Tools.

[BibT_eX]

[DOI]

Proceedings of the FPGA '21: The 2021 ACM/SIGDA International Symposium on Field Programmable Gate Arrays, Virtual Event, USA, February 28, 2021

Probabilistic Optimization for High-Level Synthesis.

[BibT_eX]

[DOI]

Proceedings of the FPGA '21: The 2021 ACM/SIGDA International Symposium on Field Programmable Gate Arrays, Virtual Event, USA, February 28, 2021

An Empirical Study of the Reliability of High-Level Synthesis Tools.

[BibT_eX]

[DOI]

Proceedings of the 29th IEEE Annual International Symposium on Field-Programmable Custom Computing Machines, 2021

Probabilistic Scheduling in High-Level Synthesis.

[BibT_eX]

[DOI]

Proceedings of the 29th IEEE Annual International Symposium on Field-Programmable Custom Computing Machines, 2021

2020

architect: Arbitrary-Precision Hardware With Digit Elision for Efficient Iterative Compute.

[BibT_eX]

[DOI]

He Li

James J. Davis

IEEE Trans. Very Large Scale Integr. Syst., 2020

Persistency semantics of the Intel-x86 architecture.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

Slow and Steady: Measuring and Tuning Multicore Interference.

[BibT_eX]

[DOI]

Dan Iorga

Proceedings of the IEEE Real-Time and Embedded Technology and Applications Symposium, 2020

Precise Pointer Analysis in High-Level Synthesis.

[BibT_eX]

[DOI]

Proceedings of the 30th International Conference on Field-Programmable Logic and Applications, 2020

Finding and Understanding Bugs in FPGA Synthesis Tools.

[BibT_eX]

[DOI]

Yann Herklotz

Proceedings of the FPGA '20: The 2020 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays, 2020

Combining Dynamic & Static Scheduling in High-level Synthesis.

[BibT_eX]

[DOI]

Paolo Ienne

Proceedings of the FPGA '20: The 2020 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays, 2020

Reasoning over Permissions Regions in Concurrent Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

Modulo Scheduling with Rational Initiation Intervals in Custom Hardware Design.

[BibT_eX]

[DOI]

Proceedings of the 25th Asia and South Pacific Design Automation Conference, 2020

2019

Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models.

[BibT_eX]

[DOI]

Azalea Raad

Viktor Vafeiadis

Proc. ACM Program. Lang., 2019

2018

Polyhedral-Based Dynamic Loop Pipelining for High-Level Synthesis.

[BibT_eX]

[DOI]

Samuel Bayliss

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2018

Scheduling Weakly Consistent C Concurrency for Reconfigurable Hardware.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 2018

The semantics of transactions and weak memory in x86, Power, ARM, and C++.

[BibT_eX]

[DOI]

Nathan Chong

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Concurrency-Aware Thread Scheduling for High-Level Synthesis.

[BibT_eX]

[DOI]

Proceedings of the 26th IEEE Annual International Symposium on Field-Programmable Custom Computing Machines, 2018

Digit Elision for Arbitrary-accuracy Iterative Computation.

[BibT_eX]

[DOI]

He Li

James J. Davis

Proceedings of the 25th IEEE Symposium on Computer Arithmetic, 2018

2017

The Semantics of Transactions and Weak Memory in x86, Power, ARMv8, and C++.

[BibT_eX]

[DOI]

Nathan Chong

CoRR, 2017

Automatically comparing memory consistency models.

[BibT_eX]

[DOI]

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

architect: Arbitrary-precision constant-hardware iterative compute.

[BibT_eX]

[DOI]

He Li

James J. Davis

Proceedings of the International Conference on Field Programmable Technology, 2017

Tile size selection for optimized memory reuse in high-level synthesis.

[BibT_eX]

[DOI]

Proceedings of the 27th International Conference on Field Programmable Logic and Applications, 2017

Hardware Synthesis of Weakly Consistent C Concurrency.

[BibT_eX]

[DOI]

Shane T. Fleming

Proceedings of the 2017 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays, 2017

Forward Progress on GPU Concurrency (Invited Talk).

[BibT_eX]

[DOI]

Jeroen Ketema

Proceedings of the 28th International Conference on Concurrency Theory, 2017

Run fast when you can: Loop pipelining with uncertain and non-uniform memory dependencies.

[BibT_eX]

[DOI]

Samuel Bayliss

Proceedings of the 51st Asilomar Conference on Signals, Systems, and Computers, 2017

2016

Overhauling SC atomics in C11 and OpenCL.

[BibT_eX]

[DOI]

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Balancing Locality and Concurrency: Solving Sparse Triangular Systems on GPUs.

[BibT_eX]

[DOI]

Proceedings of the 23rd IEEE International Conference on High Performance Computing, 2016

An efficient implementation of online arithmetic.

[BibT_eX]

[DOI]

Yiren Zhao

Proceedings of the 2016 International Conference on Field-Programmable Technology, 2016

A Case for Work-stealing on FPGAs with OpenCL Atomics.

[BibT_eX]

[DOI]

Felix Winterstein

Proceedings of the 2016 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays, 2016

Automatically Optimizing the Latency, Area, and Accuracy of C Programs for High-Level Synthesis.

[BibT_eX]

[DOI]

Xitong Gao

Proceedings of the 2016 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays, 2016

Loop Splitting for Efficient Pipelining in High-Level Synthesis.

[BibT_eX]

[DOI]

Proceedings of the 24th IEEE Annual International Symposium on Field-Programmable Custom Computing Machines, 2016

2015

The Design and Implementation of a Verification Technique for GPU Kernels.

[BibT_eX]

[DOI]

Adam Betts

Nathan Chong

ACM Trans. Program. Lang. Syst., 2015

Taming the complexities of the C11 and OpenCL memory models.

[BibT_eX]

[DOI]

CoRR, 2015

Remote-scope promotion: clarified, rectified, and verified.

[BibT_eX]

[DOI]

Bradford M. Beckmann

Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, 2015

Custom-sized caches in application-specific memory hierarchies.

[BibT_eX]

[DOI]

Proceedings of the 2015 International Conference on Field Programmable Technology, 2015

GPU Concurrency: Weak Behaviours and Programming Assumptions.

[BibT_eX]

[DOI]

Jade Alglave

Ganesh Gopalakrishnan

Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, 2015

2014

Syntax and semantics of a GPU kernel programming language.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

KernelInterceptor: automating GPU kernel verification by intercepting kernels and their parameters.

[BibT_eX]

[DOI]

Ethel Bardsley

Proceedings of the International Workshop on OpenCL, 2014

2013

Concurrent verification for sequential programs.

[BibT_eX]

[DOI]

PhD thesis, 2013

Ribbon Proofs.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2013

Ribbon Proofs for Separation Logic.

[BibT_eX]

[DOI]

Mike Dodds

Matthew J. Parkinson

Proceedings of the Programming Languages and Systems, 2013

2011

Unifying Models of Data Flow.

[BibT_eX]

[DOI]

Tony Hoare

Proceedings of the Software and Systems Safety - Specification and Verification, 2011

2010

Explicit Stabilisation for Modular Rely-Guarantee Reasoning.

[BibT_eX]

[DOI]