Photo of John Wickerson

John Wickerson

I'm a Lecturer in the Circuits and Systems group, which is part of the Department of Electrical and Electronic Engineering at Imperial College London.

My research aims to improve the reliability of high-performance computing with the help of formal methods.

NEWS: Lana Josipović and I are organising the FLASHLIGHT workshop at FCCM 2022 in New York, on Formal Methods in High-Level Synthesis. If you have an interest in formal methods or high-level synthesis (or both!), then we'd love for you to join us.

Projects

Here is a selection of research projects I am or have been involved in.

People

Current team members

  • Jianyi Cheng, PhD student since 2018 (jointly with George Constantinides)
  • Yann Herklotz, PhD student since 2019
  • Dan Iorga, PhD student since 2018 (jointly with Alastair Donaldson)
  • Vasileios Klimis, postdoc since 2021 (jointly with Alastair Donaldson)
  • Jack Clark, research assistant since 2021 (jointly with Alastair Donaldson)

Former team members

Collaborators

Recent blog articles

27-Aug-2021
High-level synthesis, but correct
03-Jul-2021
Understanding the memory semantics of multi-threaded CPU/FPGA programs
09-Jun-2021
Introducing C4: the C Compiler Concurrency Checker
07-May-2021
Fuzzing High-Level Synthesis Tools
18-Sep-2020
A translation puzzle
19-Aug-2020
People of PL: Derek Dreyer
18-Jun-2020
People of PL: Ron Garcia
03-Jun-2020
People of PL: Mike Hicks
26-May-2020
People of PL: Alexandra Silva
21-May-2020
Diagrams for composing compilers
27-Feb-2020
Highlights from FPGA 2020
19-Feb-2020
New names for odd and even functions
22-Nov-2019
Fuzzing FPGA synthesis tools
14-Nov-2019
A plot twist, part II: In praise of scatter plots
12-Nov-2019
A plot twist: Drawing better graphs in PL papers
22-Oct-2019
In praise of scatter plots
04-Oct-2019
Loop invariants – where should we put them?
05-Sep-2019
Modulo scheduling with rational initiation intervals
08-Aug-2019
How to draw block diagrams
16-Feb-2019
A wordless proof
29-Jun-2018
Greatest Hits of PLDI 2018
6-May-2018
What is the difference between latency and throughput?
4-May-2018
Greatest Hits of FCCM 2018
5-Mar-2018
Concurrency-aware scheduling for high-level synthesis
12-Feb-2018
What do you get if you cross Weak Memory with Transactional Memory?

Publications

Journal articles

TCAD 2022
Patrick Sittel, Nicolai Fiege, John Wickerson, and Peter Zipf. Optimal and heuristic approaches to modulo scheduling with rational initiation intervals in hardware synthesis. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 41:614--627, 2022.
[ DOI | pdf ]
TCAD 2022
Jianyi Cheng, Lana Josipovic, George A. Constantinides, Paolo Ienne, and John Wickerson. DASS: Combining dynamic & static scheduling in high-level synthesis. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 41:628--641, 2022.
[ DOI | pdf ]
OOPSLA 2021
Dan Iorga, Alastair F. Donaldson, Tyler Sorensen, and John Wickerson. The semantics of shared memory in Intel CPU/FPGA systems. Proc. ACM on Programming Languages, 5(OOPSLA), 2021.
[ blog | pdf ]
OOPSLA 2021
Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Formal verification of high-level synthesis. Proc. ACM on Programming Languages, 5(OOPSLA), 2021.
[ pdf ]
OOPSLA 2021
Tyler Sorensen, Lucas F. Salvador, Harmit Raval, Hugues Evrard, John Wickerson, Margaret Martonosi, and Alastair F. Donaldson. Specifying and testing GPU workgroup progress models. Proc. ACM on Programming Languages, 5(OOPSLA), 2021.
[ pdf ]
TC 2021
Jianyi Cheng, Shane Fleming, Yu Ting Chen, Jason Anderson, John Wickerson, and George A. Constantinides. Efficient memory arbitration in high-level synthesis from multi-threaded code. IEEE Transactions on Computers, 2021.
[ DOI | pdf ]
TVLSI 2021
Nadesh Ramanathan, George A. Constantinides, and John Wickerson. Global analysis of C concurrency in high-level synthesis. IEEE Trans. on Very Large Scale Integration (VLSI) Systems, 29(1):24--37, 2021.
[ DOI | pdf ]
POPL 2020
Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis. Persistency semantics of the Intel-x86 architecture. Proc. ACM on Programming Languages, 4(POPL), 2020.
[ DOI | pdf ]
TVLSI 2020
He Li, James J. Davis, John Wickerson, and George A. Constantinides. Architect: Arbitrary-precision hardware with digit elision for efficient iterative compute. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 28(2):516--529, 2020.
[ DOI | pdf ]
OOPSLA 2019
Azalea Raad, John Wickerson, and Viktor Vafeiadis. Weak persistency semantics from the ground up. Proc. ACM on Programming Languages, 3(OOPSLA), 2019.
[ DOI | pdf ]
TCAD 2018
Junyi Liu, John Wickerson, Samuel Bayliss, and George A. Constantinides. Polyhedral-based dynamic loop pipelining for high-level synthesis. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 37(9), September 2018.
[ DOI | pdf ]
TC 2018
Nadesh Ramanathan, John Wickerson, and George A. Constantinides. Scheduling weakly consistent C concurrency for reconfigurable hardware. IEEE Transactions on Computers, 67(7), July 2018.
[ DOI | pdf ]
TOPLAS 2015
Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson, and John Wickerson. The design and implementation of a verification technique for GPU kernels. ACM Trans. Programming Languages and Systems, 37(3), 2015.
[ DOI | pdf ]

Conference papers

FCCM 2022
Michalis Pardalos, Yann Herklotz, and John Wickerson. Resource sharing for verified high-level synthesis. In IEEE Int. Symp. on Field-Programmable Custom Computing Machines, 2022. Short paper category.
FCCM 2022
Jianyi Cheng, John Wickerson, and George A. Constantinides. Dynamic C-slow pipelining for HLS. In IEEE Int. Symp. on Field-Programmable Custom Computing Machines, 2022.
ESOP 2022
Eleni Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, and John Wickerson. View-based Owicki–Gries reasoning for persistent x86-TSO. In European Symposium on Programming, 2022. Distinguished Artifact award.
[ pdf ]
FPGA 2022
Jianyi Cheng, John Wickerson, and George A. Constantinides. Finding and finessing static islands in dynamically scheduled circuits. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2022.
[ pdf ]
FPL 2021
Jianyi Cheng, John Wickerson, and George A. Constantinides. Exploiting the correlation between dependence distance and latency in loop pipelining. In IEEE Int. Symp. on Field-Programmable Logic and Applications, 2021.
[ pdf ]
ISSTA 2021
Matt Windsor, Alastair F. Donaldson, and John Wickerson. C4: the C compiler concurrency checker. In ACM SIGSOFT Int. Symp. on Software Testing and Analysis, 2021. Tool demonstrations track.
[ blog | pdf ]
FCCM 2021
Yann Herklotz, Zewei Du, Nadesh Ramanathan, and John Wickerson. An empirical study of the reliability of high-level synthesis tools. In IEEE Int. Symp. on Field-Programmable Custom Computing Machines, 2021. Short paper category.
[ DOI | blog | pdf ]
FCCM 2021
Jianyi Cheng, John Wickerson, and George A. Constantinies. Probabilistic optimization for high-level synthesis. In IEEE Int. Symp. on Field-Programmable Custom Computing Machines, 2021.
[ DOI | blog | pdf ]
FPL 2020
Nadesh Ramanathan, George A. Constantinides, and John Wickerson. Precise pointer analysis in high-level synthesis. In Int. Conf. on Field Programmable Logic and Applications, 2020.
[ DOI | pdf ]
CAV 2020
James Brotherston, Diana Costa, Aquinas Hobor, and John Wickerson. Reasoning over permissions regions in concurrent separation logic. In Int. Conf. on Computer Aided Verification, 2020.
[ DOI | pdf ]
RTAS 2020
Dan Iorga, Tyler Sorensen, John Wickerson, and Alastair F. Donaldson. Slow and steady: Measuring and tuning multicore interference. In IEEE Real-Time and Embedded Technology and Applications Symposium, 2020.
[ DOI | pdf ]
FPGA 2020
Yann Herklotz and John Wickerson. Finding and understanding bugs in FPGA synthesis tools. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2020.
[ DOI | slides | blog | pdf ]
FPGA 2020
Jianyi Cheng, Lana Josipović, George A. Constantinides, Paolo Ienne, and John Wickerson. Combining dynamic and static scheduling in high-level synthesis. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2020.
[ DOI | pdf ]
ASP-DAC 2020
Patrick Sittel, John Wickerson, Martin Kumm, and Peter Zipf. Modulo scheduling with rational initiation intervals in custom hardware design. In Asia and South Pacific Design Automation Conference, 2020. Nominated for Best Paper award.
[ DOI | blog | pdf ]
ARITH 2018
He Li, James J. Davis, John Wickerson, and George A. Constantinides. Digit elision for arbitrary-accuracy iterative computation. In IEEE Symp. on Computer Arithmetic, 2018.
[ DOI | pdf ]
PLDI 2018
Nathan Chong, Tyler Sorensen, and John Wickerson. The semantics of transactions and weak memory in x86, Power, ARM, and C++. In ACM Conf. on Programming Language Design and Implementation, 2018. Distinguished Paper award.
[ DOI | press | slides | blog | pdf ]
FCCM 2018
Nadesh Ramanathan, George A. Constantinides, and John Wickerson. Concurrency-aware thread scheduling for high-level synthesis. In IEEE Int. Symp. on Field-Programmable Custom Computing Machines, 2018. Runner-up, Best Paper award.
[ DOI | blog | pdf ]
FPT 2017
He Li, James J. Davis, John Wickerson, and George A. Constantinides. ARCHITECT: Arbitrary-precision constant-hardware iterative compute. In Int. Conf. on Field-Programmable Technology, 2017. Best Paper Presentation award.
[ DOI | pdf ]
FPL 2017
Junyi Liu, John Wickerson, and George A. Constantinides. Tile size selection for optimized memory reuse in high-level synthesis. In Int. Conf. on Field Programmable Logic and Applications, 2017.
[ DOI | pdf ]
FPGA 2017
Nadesh Ramanathan, Shane T. Fleming, John Wickerson, and George A. Constantinides. Hardware synthesis of weakly consistent C concurrency. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2017.
[ DOI | slides | blog | pdf ]
POPL 2017
John Wickerson, Mark Batty, Tyler Sorensen, and George A. Constantinides. Automatically comparing memory consistency models. In ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, 2017.
[ DOI | tex | poster | additional material | video | slides | blog | pdf ]
HiPC 2016
Andrea Picciau, Gordon E. Inggs, John Wickerson, Eric C. Kerrigan, and George A. Constantinides. Balancing locality and concurrency: solving sparse triangular systems on GPUs. In IEEE Int. Conf. on High Performance Computing, Data, and Analytics, 2016.
[ DOI | pdf ]
FPT 2016
Yiren Zhao, John Wickerson, and George A. Constantinides. An efficient implementation of online arithmetic. In Int. Conf. on Field-Programmable Technology, 2016.
[ DOI | pdf ]
FCCM 2016
Junyi Liu, John Wickerson, and George A. Constantinides. Loop splitting for efficient pipelining in high-level synthesis. In IEEE Int. Symp. on Field-Programmable Custom Computing Machines, 2016.
[ DOI | pdf ]
FPGA 2016
Nadesh Ramanathan, John Wickerson, Felix Winterstein, and George A. Constantinides. A case for work-stealing on FPGAs with OpenCL atomics. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2016. Short paper category.
[ DOI | pdf ]
FPGA 2016
Xitong Gao, John Wickerson, and George A. Constantinides. Automatically optimizing the latency, area, and accuracy of C programs for high-level synthesis. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2016.
[ DOI | pdf ]
POPL 2016
Mark Batty, Alastair F. Donaldson, and John Wickerson. Overhauling SC atomics in C11 and OpenCL. In ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, 2016.
[ DOI | tex | additional material | video | slides | pdf ]
FPT 2015
Felix Winterstein, Kermin Fleming, Hsin-Jung Yang, John Wickerson, and George A. Constantinides. Custom-sized caches in application-specific memory hierarchies. In Int. Conf. on Field-Programmable Technology, 2015.
[ DOI | pdf ]
OOPSLA 2015
John Wickerson, Mark Batty, Bradford M. Beckmann, and Alastair F. Donaldson. Remote-scope promotion: Clarified, rectified, and verified. In ACM SIGPLAN Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications, 2015.
[ DOI | tex | additional material | video | slides | pdf ]
ASPLOS 2015
Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, and John Wickerson. GPU concurrency: Weak behaviours and programming assumptions. In ACM Int. Conf. on Architectural Support for Programming Languages and Operating Systems, 2015.
[ DOI | additional material | pdf ]
IWOCL 2014
Ethel Bardsley, Alastair F. Donaldson, and John Wickerson. KernelInterceptor: Automating GPU kernel verification by intercepting kernels and their parameters. In Int. Workshop on OpenCL, 2014.
[ DOI | pdf ]
ESOP 2013
John Wickerson, Mike Dodds, and Matthew J. Parkinson. Ribbon proofs for separation logic. In Europ. Symp. on Programming, 2013.
[ DOI | tex | slides | pdf ]
ESOP 2010
John Wickerson, Mike Dodds, and Matthew J. Parkinson. Explicit stabilisation for modular rely-guarantee reasoning. In Europ. Symp. on Programming, 2010.
[ DOI | tex | slides | pdf ]

Other publications and presentations

LATTE 2021
Yann Herklotz and John Wickerson. High-level synthesis tools should be proven correct. In Workshop on Languages, Tools, and Techniques for Accelerator Design, 2021.
[ video | pdf ]
MET 2021
Andrei Lascu, Matt Windsor, Alastair F. Donaldson, Tobias Grosser, and John Wickerson. Dreaming up metamorphic relations: Experiences from three fuzzer tools. In Int. Workshop on Metamorphic Testing, 2021.
[ pdf ]
USENIX ATC 2019
Nathan Chong, Tyler Sorensen, and John Wickerson. The semantics of transactions and weak memory in x86, Power, ARM, and C++. In USENIX Annual Technical Conference, 2019. Invited paper in the Best of the Rest track.
[ video | slides | pdf ]
DHPCC++ 2018
John Wickerson. Journey to the centre of the OpenCL memory model. In Workshop on Distributed and Heterogeneous Programming in C and C++, 2018. Keynote Address.
[ slides ]
FMATS 2018
John Wickerson. Towards verified hardware compilation. In Sixth Workshop on Formal Methods and Tools for Security, 2018.
[ slides ]
2018
John Wickerson and George A. Constantinides. From irregular heterogeneous software to reconfigurable hardware. In Bashir Al-Hashimi and Geoff Merrett, editors, Many Core Computing: Hardware and Software. IET Press, 2018.
[ DOI ]
ACSSC 2017
Junyi Liu, John Wickerson, Samuel Bayliss, and George A. Constantinides. Run fast when you can: Loop pipelining with uncertain and non-uniform memory dependencies. In Asilomar Conf. on Signals, Systems and Computers, 2017. Invited paper.
[ DOI | pdf ]
CONCUR 2017
Alastair F. Donaldson, Jeroen Ketema, Tyler Sorensen, and John Wickerson. Forward progress on GPU concurrency. In Int. Conf. on Concurrency Theory, 2017. Invited paper.
[ DOI | pdf ]
2013
John Wickerson. Ribbon proofs and dynamically-scoped quantifiers. Unpublished note, 2013.
[ pdf ]
2013
John Wickerson. Concurrent Verification for Sequential Programs. PhD thesis, University of Cambridge, July 2013.
[ DOI | pdf ]
LICS 2012
John Wickerson, Mike Dodds, and Matthew J. Parkinson. Ribbon proofs for separation logic. In ACM/IEEE Symp. on Logic in Computer Science, 2012. Short paper category.
[ slides | pdf ]
2011
Tony Hoare and John Wickerson. Unifying models of data flow. In Manfred Broy, Christian Leuxner, and Tony Hoare, editors, Software and Systems Safety. IOS Press, 2011.
[ DOI | slides | pdf ]
2009
John Wickerson. Partial and total correctness as greatest and least fixed points. Unpublished note, 2009.
[ pdf ]
2008
John Wickerson. Nominal prolog. Final-year (Part II) dissertation, University of Cambridge, July 2008.
[ pdf ]

Professional service

Conference and workshop organisation:

2021
ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI), publicity chair
2020
ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI), publicity chair
2015
Imperial Concurrency Workshop, co-organiser

Program/review committee member:

2022
ACM Symp. on Principles of Programming Languages (POPL)
ACM SIGSOFT Int. Symp. on Software Testing and Analysis (ISSTA)
IEEE Int. Symp. on Field-Programmable Custom Computing Machines (FCCM)
2021
ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)
Europ. Conf. on Object-Oriented Programming (ECOOP)
IEEE Int. Symp. on Field-Programmable Custom Computing Machines (FCCM)
2020
ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)
IEEE Int. Symp. on Field-Programmable Custom Computing Machines (FCCM)
2019
Europ. Conf. on Object-Oriented Programming (ECOOP), external review committee
ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI)
Asia and South Pacific Design Automation Conference (ASP-DAC)
Designer Track, Design Automation Conference (DAC)
Field-Programmable Logic and Applications (FPL)
2018
Reengineering for Parallelism in Heterogeneous Parallel Platforms (RePara)
Designer Track, Design Automation Conference (DAC)
Field-Programmable Logic and Applications (FPL)
2017
Field-Programmable Logic and Applications (FPL)
2016
Reengineering for Parallelism in Heterogeneous Parallel Platforms (RePara)
Tiny Transactions on Computer Science (TinyTOCS)
2015
Automated Verification of Critical Systems (AVoCS)
Reengineering for Parallelism in Heterogeneous Parallel Platforms (RePara)

Artifact evaluation committee member:

2015
ACM Symp. on Principles of Programming Languages (POPL)

Reviewer for the following conferences and journals:

2021
ACM Trans. on Reconfigurable Technology and Systems (TRETS)
ACM Trans. on Programming Languages and Systems (TOPLAS)
2020
ACM Trans. on Reconfigurable Technology and Systems (TRETS)
2019
Science of Computer Programming
2018
IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems (TCAD)
IEEE Int. Symp. on Field-Programmable Custom Computing Machines (FCCM)
IEEE Int. Conf. on Software Testing, Verification and Validation (ICST)
ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI)
2017
ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays (FPGA)
Journal of Supercomputing
Symp. on Parallelism in Algorithms and Architectures (SPAA)
2016
ACM Trans. on Computational Logic (TOCL)
ACM Trans. on Reconfigurable Technology and Systems (TRETS)
ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)
ACM Symp. on Principles of Programming Languages (POPL)
ACM Symp. on Principles and Practice of Parallel Programming (PPoPP)
2015
Int. Conf. on Computer Aided Verification (CAV)
Europ. Symp. on Programming (ESOP)
ACM Symp. on Principles of Programming Languages (POPL)
ACM Symp. on Principles and Practice of Parallel Programming (PPoPP)
2014
Joint Int. Conf. on Rewriting and Typed Lambda Calculi (RTA-TLCA)
Int. Conf. on Runtime Verification (RV)
Static Analysis Symp. (SAS)
2012
ACM Int. Conf. on Certified Programs and Proofs (CPP)
Int. Conf. on Relational and Algebraic Methods in Computer Science (RAMiCS)
Symp. on Parallelism in Algorithms and Architectures (SPAA)
Int. Conf. on Verified Software: Theories, Tools, and Experiments (VSTTE)
2011
Int. Conf. on Computer Aided Verification (CAV)
2010
Europ. Symp. on Programming (ESOP)
ACM/IEEE Symp. on Logic in Computer Science (LICS)
ACM Symp. on Principles of Programming Languages (POPL)
Int. Conf. on Verified Software: Theories, Tools, and Experiments (VSTTE)
2009
ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI)

Teaching and other roles

Current teaching

Previous teaching

  • Lecturer for a module on Language Processors for second-year EIE students (2019‐2020)
  • Guest lecturer for a module on Models of Computation for second-year computing students (2016)

Other roles

Some fun stuff

Contact

email
j.wickersonXimperial.ac.uk (replace X with @)

mail
Dr John Wickerson
Department of Electrical and Electronic Engineering
Imperial College London
South Kensington Campus
London
SW7 2AZ
desk
Room 913
9th Floor
Department of Electrical and Electronic Engineering
(wacky.laptop.sizes)

social