γγγγγγγγγγγγγγγγ γ γ γ {γ γγ /γγ½
γγγγγγγγγγγγγγγ γ γ γ γ γ½γγ/ γΒ¨ο½οΎ- ββγ-βββο½€_
γγγγγγγγγγγ γ _γ- βββ-ο½€ββο½οΌ /Β΄ο½γ½γ,_γ€Β΄γγγοΌγ/7β-ο½€
γγγγγγγγγγγοΌ γ γ γ γ γ lγοΌγγγ γ οΌ /Β΄γγγ/γγlγlγγl
γγγγγγγγγγγγγγγγ οΌΏ οΌ'γγοΌΒ΄ |γε
«γγ/οΌγγγγγγͺγγγ|γ½
γγγγγγγγγγ__γ- δΊοΏ£γ γ γ οΌγ/ ε
«γ γ β¨οΌ/ οΌ|/β¨lγ οΎγγγγΈ
γγγγγγγγ, -γγγγγγγγγ οΌlγ β§ γ οΌΌγγγ /|/γεγοΎγγ γ½γγ γ
γγγ,γγΒ΄ οΌ οΌγγγΈοΌΏ οΌ- Β΄ οΌοΌl ./οΌΌ ,γΈ/ γγ, ｨｺο½ο½€ γ½| |γN|γγγγ οΎ
γοΌ γ γ /οΌγ ,γγΒ΄γγγ γ οΌοΌ / l/γ| ο½ (οΎο½|γγγεΌ!οΎγγi/β¨γ|γ γ γ }
/γγγ οΌlγ οΌ /)γ ,ο½€.γγγ /οΌ/ /γ ! γlγγ½__γ γ γ ο½γΒ΄ γγγο½€!|γ/ ο½γ/
!γγ.οΌγ οΌ γ/.οΎ ./ οΎ/ )γ /γ / /γγlγ l γ |γγγγγγγγγγlο½ΏοΎ !/οΌlβ§
γοΌ/γοΌ/γ οΌγl.lΒ΄/ / /γ/οΌΏο½γο½γγ ! γγ lγγγ γγ lοΌΌγο½€ / / β§γ.οΎγγ½
/γ/οΌγ/ γ γγlγ!/γlοΌ ,-β'γγοΌΌγ!'γγ / γ δΈΆγ γ γ½_γ½γ δΊΊ οΌΌγγγ γ γ γ,γ,ο½€,ο½€
! .//γ ο½.γ γ.γlγ__γγγοΌοΌγοΌΌοΌΌ_οΎ !γγ,t=ο½ͺο½ͺx_ οΌΌγγ γ οΌ|γ οΌΌ οΌΌγγγγ οΌοΎ/οΎl | γ ,
γl/ γγ',.γγγ |/::::| γ /οΌ οΌβ ο½γΌο½γ½γ/ β:β γΎ __.lγγ£οΌΒ΄l !γγ |οΌΌ ο½ο½°β β§/7δΊ .οΎ
οΌοΎοΎο½γ½
. ο½γ γ γ γ γ l|::::/γ /γοΌγ/(βοΌ|:οΌΌ οΎγ½γ γ γ γ β¨| οΌΏ,-β!β ο½€ε
«γ οΌΌ_οΌ/ |//:::::οΏ£οΌ
γ οΌΌγγ γ γ / Vγ /οΌγγγγγγ |:::::::γγδΈΆοΏ£οΌΌ_ γ / οΌΏγοΌΌοΌΏ β§γγ½γγγ/γγ:::::::::::l
γγγγγγγ γ γγγlγ/γγ/οΌΏγ οΌ::::/γ /οΏ£ `γΌο½€οΌΌοΌ ,ο½²γοΌΌl:::|γ lγγ ο½γΌ' γ lγ !::::::::l
γγγγγοΌγ_β¨οΌΏ γ½/γγ/γοΌ::::::::::/γοΌοΌΒ΄ο½γ½γοΌΌ_οΌγγ, -βο½€γ½γlγγγγγγ |γ οΏ£ /
γγγγ/γγγγγββγγ /. /:::::::::::::/γ/ /γγγγγο½γ½ οΌοΌ γγ γ οΌΌ. lγγγγ/βο½β-γ/
.γ γ /γγ/. ο½ο½°t-γγ|γ ///::::::::::::/γ lγl: : : : : : : : : . .}γγ l. . . : : : : }::|γγγγοΌΌοΌΌγγγ½
γγ / γ /γ γ .|γ γ | ./ο½€/:::::::::::::/γγl ε
«: : : : : : : : οΌ'γγγο½οΌ: : :/:::iγγγγγ/γ γ οΌ
.γ /γγο½γγ γ |γ γ l/::::::::::::::::::/γγγlγγο½γΌβ Β΄οΌΌγγγ γγ|οΏ£|:::::::lγγγγ/γ γ /
γ/ γ γ οΎ/οΌγ|γ γ l::::::::::::::::::/οΌΌγγ lγγγγγγγγοΌΌγγγγlγ ο½:::::::lγγγ/!γ γ /
. {γγγγ/ l / γο½γγγl:::::::::::::::/lγγοΌΌγοΌΌγγ' οΌ([]) οΌ,γ οΌΌ.γγ/γγγ::::lγγ/:::ο½γγ /
γοΌΌγγ/γl γγ.l γ β§!:::::::::::/γ!β§ γ οΌΌ/γγο½γΌ-β'γγ γ οΌΌ/ γ `ο½:::::lγ/:::::::l γ ο½Ώ
γγγγl γ ο½γγ iγγ|::οΎ:::::::::β§γlγβ¨οΌΌ|: οΌΌγγγγοΌΏ γ γ γ β¨γγV:::!/::::::::/γ /
γγγγl γ οΎο½€γ lγγl::::οΎ:::::/γ οΌΌγγγγ!γγοΌΌγγ γ οΏ£γγ γ οΎ.γ γVl::::::::::lγ /
γγγγl γ lγγ |γγl::::β§/γγ γ οΌΌγγ,οΎγγͺ/γ½β _γγγγγγγ' , γ γγοΌγ/
γγ γ οΎγ lγ γ|γγl:/ ./ γ γ γ γ ο½γ½γγγγγ οΌΌγ οΌΏγγγγγγοΌΌ γγο½€__/
γγγγγοΌΌ γ γοΌΌοΌΏγγγγγγ γ γ γ γ γ γ γ |/Β΄γγ ο½γ½γγγγ ' , γ οΎ
γγγγγγγγγγγγγγγγγγγγγ γ γ γ γ γ llγγγγγ β§γγγγ ' ,γο½.οΎ
γγγγγγγγγγγγγγγγγγγγγγγγγγγγ ο½|γγγγγγγ' ,γ γγγ', .lγοΎ
γγγγγγγγγγγγγγγγγγγγγγγγγ γ γ |lγγ γ γ γ γ '., γγγ iγlγ οΎ
γγγγγγγγγγγγγγγγγγγ γ γ γ γ γ γ lγγγγγγγγγγ,γ γγlγlγγοΎ
γγγγγγγγγγγγγγγγγγγγγγγγγγγγlγγγγγοΌΏγγγγ , γγ lγlγ γοΎ
γγγγγγγγγγγγγγγγγγγγ γ γ γ γ γ lγγγγγγγοΏ£δΊδΈΆ',γ γ|γl γγγ
γγγγγγγγγγγγγγγγγ γ γ γ γ γ γ γ |γγγγγγ γ γ γ ο½γ½.γ |γο½γγγβ§
γγγγγγγγγγγγγγγγγ γ γ γ γ γ γ γ lγγγγγγγγγγγγγοΌΌ γγ γγ β§
γγγγγγγγγγγγγγγγγγγγγγγγγγγ lοΌΏοΌΏοΌΏοΌΏοΌΏοΌΏ γ οΌΏ.γγοΌΌγγγγ β§
γγγγγγγγγγγγγγγγγγγγγγγγγγγγοΌΏ:::::::::::::::::::::::::::βββ::::::::::οΌΌγ γ β§Ph.D. student in Computer Science & Engineering at UC Santa Cruz
Zheyuan Chen is a Ph.D. student in Computer Science & Engineering at UC Santa Cruz working on GPU semantics, formal verification, portable GPU kernels, and ML systems.
Iβm Zheyuan Chen, a Ph.D. student in Computer Science & Engineering at the University of California, Santa Cruz. Iβm advised by Prof. Tyler Sorensen and work on GPU semantics, formal methods, compilers, and portable ML kernels.
I am particularly interested in GPU semantics and highly efficient portable kernel design. I believe that the lack of precise, formal semantics in current GPU programming models, especially around subgroup execution, synchronization, and memory consistency, limits our ability to reason about correctness and performance portability. My research aims to develop formal foundations and practical tools for rigorous reasoning about GPU behavior, and to leverage these insights to design portable kernels that achieve both correctness and high performance across heterogeneous architectures.
One way to summarize the kind of systems work I like is:
struct Research {
focus: [GpuSemantics, FormalVerification, PortableKernels],
}
impl Research {
fn optimize(&self) -> Goal {
semantics::model(SubgroupBehavior)
.verify_with(FormalMethod)
.compile_to(PortableGpuKernel)
}
}
const GOAL: &str = "Correct and fast kernels across architectures";The quickest way to navigate this site is through my publications, CV, and public code on GitHub.
Updates
View allResearch
View allSIMT-Step provides a formal and flexible operational semantics for GPU subgroup execution, using dynamic basic blocks and TLA+ validation to reason about converged, synchronous, and independent behaviors across devices.
BetterTogether enables fine-grained software pipelining on heterogeneous edge SoCs using a profile-guided performance model that captures intra-application interference across CPUs and GPUs.
sqlelf models ELF objects as relational databases, enabling expressive SQL queries, aggregation, and cross-object analysis for more accessible and efficient ELF exploration.
Teaching