arXiv subjects

Ke Du

Publications and source records attributed to Ke Du.

7 recordsLinked to original sources

arXiv2026

A Formal Semantics of C with OpenMP Parallelism (Extended Version)

OpenMP is a popular parallelization framework that lets users transform sequential code into parallel code with a few simple annotations. Unfortunately, it is also easy to inadvertently introduce errors by adding OpenMP pragmas into otherwise correct programs, including both logic errors and race conditions. We present a formal semantics for C code with OpenMP directives, building on the C semantics of the CompCert verified compiler and its extension to concurrency. Our semantics captures subtle interactions between OpenMP directives and variable state that have been obscured by previous OpenMP semantics, and provides a basis for detecting undesired behaviors introduced by incorrect annotations: in particular, any successful execution is guaranteed to be free of data races.

cs.DC↗

arXiv2026

Recursive Mutexes in Separation Logic

Mutexes (i.e., locks) are well understood in separation logic, and can be specified in terms of either protecting an invariant or atomically changing the state of the lock. In this abstract, we develop the same styles of specifications for \emph{recursive} mutexes, a common variant of mutexes in object-oriented languages such as C++ and Java. A recursive mutex can be acquired any number of times by the same thread, and our specifications treat all acquires/releases uniformly, with clients only needing to determine whether they hold the mutex when accessing the lock invariant.

cs.PL↗

arXiv2025

DORAEMON: A Unified Library for Visual Object Modeling and Representation Learning at Scale

DORAEMON is an open-source PyTorch library that unifies visual object modeling and representation learning across diverse scales. A single YAML-driven workflow covers classification, retrieval and metric learning; more than 1000 pretrained backbones are exposed through a timm-compatible interface, together with modular losses, augmentations and distributed-training utilities. Reproducible recipes match or exceed reference results on ImageNet-1K, MS-Celeb-1M and Stanford online products, while one-command export to ONNX or HuggingFace bridges research and deployment. By consolidating datasets, models, and training techniques into one platform, DORAEMON offers a scalable foundation for rapid experimentation in visual recognition and representation learning, enabling efficient transfer of research advances to real-world applications. The repository is available at https://github.com/wuji3/DORAEMON.

cs.CV↗

arXiv2023

Moment-based space-variant Shack-Hartmann wavefront reconstruction

Based on image moment theory, an approach for space-variant Shack-Hartmann wavefront reconstruction is presented in this article. The relation between the moment of a pair of subimages and the local transformation coefficients is derived. The square guide 'star' is used to obtain a special solution from this relation. The moment-based wavefront reconstruction has a reduced computational complexity compared to the iteration-based algorithm. Image restorations are executed by the tiling strategy with 5 $\times$ 5 PSFs as well as the conventional strategy with a global average PSF. Visual and quantitative evaluations support our approach.

physics.optics↗

arXiv2022

Effects of Shape on Interaction Dynamics of Tetrahedral Nanoplastics and the Cell Membrane

Cellular uptake of nanoplastics is instrumental in their environmental accumulation and transfer to humans through the food chain. Despite extensive studies using spherical plastic nanoparticles, the influence of the morphological characteristics of environmentally released nanoplastics is understudied. Using dissipative particle dynamics simulations, we modeled the interactions between a cell membrane and hydrophobic nanotetrahedra, which feature high shape anisotropy and large surface curvature seen for environmental nanoplastics. We observe robust uptake of nanotetrahedra with sharp vertices and edges by the lipid membrane. Two local energy minimum configurations of nanotetrahedra embedded in the membrane bilayer were identified for particles of large sizes. Further analysis of particle dynamics within the membrane shows that the two interaction states exhibit distinct translational and rotational dynamics in the directions normal and parallel to the plane of the membrane. The membrane confinement significantly arrests the out-of-plane motion, resulting in caged translation and subdiffusive rotation. While the in-plane diffusion remains Brownian, we find that the translational and rotational modes decouple from each other as the particle size increases. The rotational diffusion decreases by a greater extent compared to the translational diffusion, deviating from the continuum theory predictions. These results provide fundamental insights into the shape effect on the nanoparticle dynamics in crowded lipid membranes.

cond-mat.soft↗

arXiv2022

Space-variant Shack-Hartmann wavefront sensing based on affine transformation estimation

The space-variant wavefront reconstruction problem inherently exists in deep tissue imaging. In this paper,we propose a framework of Shack-Hartmann wavefront space-variant sensing with extended source illumination. The space-variant wavefront is modeled as a four-dimensional function where two dimensionsare in the spatial domain and two in the Fourier domain with priors that both gently vary. Here, the affinetransformation is used to characterize the wavefront space-variant function. Correspondingly, the zonaland modal methods are both escalated to adapt to four-dimensional representation and reconstruction.Experiments and simulations show double to quadruple improvements in space-variant wavefront reconstruction accuracy compared to the conventional space-invariant correlation method.

physics.optics↗

arXiv2020

RustViz: Interactively Visualizing Ownership and Borrowing

Rust is a systems programming language that guarantees memory safety without the need for a garbage collector by statically tracking ownership and borrowing events. The associated rules are subtle and unique among industry programming languages, which can make learning Rust more challenging. Motivated by the challenges that Rust learners face, we are developing RustViz, a tool that allows teachers to generate an interactive timeline depicting ownership and borrowing events for each variable in a Rust code example. These visualizations are intended to help Rust learners develop an understanding of ownership and borrowing by example. This paper introduces RustViz by example, shows how teachers can use it to generate visualizations, describes learning goals, and proposes a study designed to evaluate RustViz based on these learning goals.

cs.PL↗