Publications
@inproceedings{provable-data-races:places22,
author = {Cogumbreiro, Tiago and Lange, Julien and Liew, Dennis and Zicarelli, Hannah},
title = {Memory Access Protocols: Certified Data-Race Freedom for {GPU} Kernels},
journal = {FMSD},
year = {2023},
doi = {10.1007/s10703-023-00415-0},
note = {[ \href{https://umb-svl.gitlab.io/assets/slides/liew.cogumbreiro.lange-provable-data-races-slides.pdf}{presentation slides} ]},
url = {assets/liew.cogumbreiro.lange-provable-data-races.pdf}
}
@inproceedings{provable-data-races:places22,
author = {Liew, Dennis and Cogumbreiro, Tiago and Lange, Julien},
title = {Provable {GPU} Data-Races in Static Race Detection},
booktitle = {PLACES},
year = {2022},
series = {EPTCS},
optvolume = {??},
optpages = {??},
optdoi = {10.48550/arXiv.2203.12878},
note = {[ \href{https://umb-svl.gitlab.io/assets/slides/liew.cogumbreiro.lange-provable-data-races-slides.pdf}{presentation slides} ]},
url = {assets/liew.cogumbreiro.lange-provable-data-races.pdf}
}
@inproceedings{gpu-eval-challenges:places22,
author = {Zicarelli, Hannah and Cogumbreiro, Tiago},
title = {Verification of {GPU} Programs: Evaluation Challenges (Extended Abstract)},
booktitle = {PLACES},
year = {2022},
note = {[ \href{https://umb-svl.gitlab.io/assets/slides/zicarelli.cogumbreiro_gpu-eval-challenges_slides.pdf}{presentation slides} ]},
url = {assets/zicarelli.cogumbreiro_gpu-eval-challenges.pdf}
}
@inproceedings{cogumbreiro:faial,
author = {Cogumbreiro, Tiago and Lange, Julien and Liew Zhen Rong, Dennis and Zicarelli, Hannah},
title = {Checking Data-Race Freedom of {GPU} Kernels, Compositionally},
booktitle = {CAV},
year = {2021},
pages = {403--426},
volumne = {12759},
doi = {10.1007/978-3-030-81685-8_19},
publisher = {Springer},
url = {assets/cogumbreiro-etal-faial.pdf},
note = {\href{https://doi.org/10.5281/zenodo.4711923}{\textbf{Artifact awarded functional, available, reusable}; includes source code and Coq proofs}
\href{https://ucl-pplv.github.io/CAV21/poster_P_195/}{[video]}}
}
@inproceedings{voss:transitive-joins,
author = {Voss, Caleb and Cogumbreiro, Tiago and Sarkar, Vivek},
title = {Transitive Joins: A Sound and Efficient Online Deadlock-avoidance Policy},
booktitle = {PPoPP},
year = {2019},
isbn = {978-1-4503-6225-2},
pages = {378--390},
numpages = {13},
doi = {10.1145/3293883.3295724},
acmid = {3295724},
publisher = {ACM},
keywords = {deadlock avoidance, futures, task parallelism}
}
@inproceedings{cogumbreiro:armus-toplas,
author = {Tiago Cogumbreiro and
Raymond Hu and
Francisco Martins and
Nobuko Yoshida},
title = {Dynamic deadlock verification for general barrier synchronisation},
booktitle = {TOPLAS},
year = {2018},
optdoi = {10.1145/XXX},
publisher = {ACM},
optpages = {150–160},
numpages = {38},
note = {Accepted. \href{assets/cogumbreiro-armus-toplas18.pdf}{Preprint PDF.}}
}
@article{cogumbreiro:gorn,
author = {Tiago Cogumbreiro and
Rishi Surendran and
Francisco Martins and
Vivek Sarkar and
Vasco T. Vasconcelos and
Max Grossman},
title = {Deadlock Avoidance in Parallel Programs with Futures: Why parallel tasks should not wait for strangers},
journal = {Proceedings of the ACM on Programming Languages},
number = {OOPSLA},
year = {2017},
publisher = {ACM},
volume = 1,
articleno = 103,
doi = {10.1145/3143359},
url = {assets/cogumbreiro-gorn.pdf},
note = {\href{https://gitlab.com/cogumbreiro/gorn/tree/oopsla17}{Source code and proof scripts}}
}
@inproceedings{murthy:dist-phasers,
author = {Karthik Murthy and
Sri Raj Paul and
Kuldeep S. Meel and
Tiago Cogumbreiro and
John M. Mellor{-}Crummey},
title = {Design and verification of distributed phasers},
booktitle = {EuroPAR},
year = {2016},
pages = {405–418},
publisher = {Springer},
series = {LNCS},
volume = {9833},
doi = {10.1007/978-3-319-43659-3_30},
url = {http://link.springer.com/chapter/10.1007%2F978-3-319-43659-3_30}
}
@inproceedings{cogumbreiro:phase-ordering,
author = {Tiago Cogumbreiro and
Jun Shirako and
Vivek Sarkar},
title = {Formalization of phase ordering},
booktitle = {PLACES},
year = {2016},
series = {EPTCS},
volume = {211},
pages = {13–24},
doi = {10.4204/EPTCS.211.2},
note = {\href{https://github.com/cogumbreiro/habanero-coq/tree/places16}{Proof scripts}},
url = {assets/cogumbreiro-phase-ordering.pdf}
}
@inproceedings{cogumbreiro:armus,
author = {Tiago Cogumbreiro and
Raymond Hu and
Francisco Martins and
Nobuko Yoshida},
title = {Dynamic deadlock verification for general barrier synchronisation},
booktitle = {PPoPP},
year = {2015},
doi = {10.1145/2688500.2688519},
publisher = {ACM},
pages = {150–160},
numpages = {11},
note = {\href{https://bitbucket.org/cogumbreiro/armus/wiki/PPoPP15}{Source code}. \href{https://bitbucket.org/cogumbreiro/brenner-coq/commits/tag/v1.0}{Proof scripts}},
url = {assets/cogumbreiro-armus.pdf}
}
@inproceedings{cogumbreiro:coordinating-phased-acts,
author = {Tiago Cogumbreiro and
Francisco Martins and
Vasco Thudichum Vasconcelos},
title = {Coordinating phased activities while maintaining progress},
booktitle = {COORDINATION},
volume = {7890},
year = {2013},
pages = {31–44},
doi = {10.1007/978-3-642-38493-6_3},
publisher = {Springer},
url = {assets/cogumbreiro.martins.vasconcelos_coordinating-phased-acts.pdf}
}
@inproceedings{martins:types-x10-clocks,
author = {Francisco Martins and Vasco T. Vasconcelos and Tiago Cogumbreiro},
title = {Types for {X10} {C}locks},
booktitle = {PLACES},
year = {2010},
pages = {111–129},
doi = {10.4204/EPTCS.69.8},
volume = {69},
series = {EPTCS},
url = {assets/martins.vasconcelos.cogumbreiro_types-for-x10-clocks.pdf}
}
@inproceedings{vasconcelos:type-inference-mil,
author = {Vasco T. Vasconcelos and Francisco Martins and Tiago Cogumbreiro},
title = {Type inference for deadlock detection in a multithreaded typed assembly language},
booktitle = {PLACES},
optbooktitle = {PLACES'09},
year = {2010},
pages = {95–109},
volume = 17,
series = {EPTCS},
url = {assets/vasconcelos.martins.cogumbreiro_type-inference-mil.pdf},
doi = {10.4204/EPTCS.17.8}
}
@inproceedings{cogumbreiro:compiling-pi-into-mtal,
author = {Tiago Cogumbreiro and Francisco Martins and Vasco T. Vasconcelos},
title = {Compiling the $pi$-calculus into a multithreaded typed assembly language},
series = {ENTCS},
volume = {241},
pages = {57–84},
year = {2009},
booktitle = {PLACES},
optbooktitle = {PLACES'08},
issn = {1571-0661},
doi = {10.1016/j.entcs.2009.06.004},
url = {assets/cogumbreiro.martins.vasconcelos_compiling-pi-into-mtal.pdf}
}