Searcharxiv⌕ Search

arXiv subjects

Jinhua Wu

Publications and source records attributed to Jinhua Wu.

6 recordsLinked to original sources

Degraded but Not Entirely Ineffective: PE-Based Deformable Graph Neural Networks

Many real-world scenarios can be represented using graph-structured data. However, traditional GNNs that transmit messages based on first-order neighbors have long faced several fundamental contradictions: increasing depth leads to over-smoothing, long-range dependencies cause over-compression, fixed neighborhoods restrict the receptive field, and on heterophilous graphs, topological neighbors become a source of noise. Although many works have addressed these issues individually, few mechanisms can simultaneously alleviate all of these challenges. To address the aforementioned problems, we propose a Position Encoding-Based Deformable Spatial Aggregation Module (PEBDSAM) that solves them all in one step. Specifically, we utilize a deformable mechanism in the position space to identify relevant nodes to supplement the original first-order neighbor information of GNNs, allowing traditional GNNs to adapt to heterophilous scenarios. Through diagnostic experiments, we obtained several major findings: current offsets fail to have any effect; subsequently, we analyzed the causes of offset failure and why model performance still improves even after offset failure, pointing out future research directions. Based on these diagnostic experiments, we streamlined the original PEBDSAM, resulting in a simplified version, which we call the Position Encoding-Based Spatial Aggregation Module (PEBSAM). In addition, we propose a PEBSAM-Speed to adapt to large datasets. Finally, we designed the module to be plug-and-play and applied it to GCN, GAT, GIN, and GraphSAGE, achieving desirable results on three homophilous datasets and six heterophilous graph datasets.

cs.AI↗

RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust

We present our ongoing work on developing an end-to-end verified Rust compiler based on CompCert. It provides two guarantees: one is semantics preservation from Rust to assembly, i.e., the behaviors of source code includes the behaviors of target code, with which the properties verified at the source can be preserved down to the target; the other is memory safety ensured by the verifying compilation -- the borrow checking pass, which can simplify the verification of Rust programs, e.g., by allowing the verification tools focus on the functional correctness.

cs.PL↗

New record in optical gain and room-temperature nanolasers in multiple wavelengths in 2D ErOCl single crystals

Erbium-based materials have long been recognized for their important telecom-band applications, yet their widespread adoption in integrated optoelectronics has been hindered by two fundamental limitations: the difficulty in achieving high erbium density without concentration quenching which leads to small optical gain in doped materials, and the difficulty in fabricating a practical device with single crystal nanowires that demonstrated high optical gain previously1,2. Here, we overcome these limitations by synthesizing 2D single crystal ErOCl that has an Er density of 1.75*1022 cm-3. The high-quality single crystal material significantly reduces the density-related quenching effect that dominates in randomly doped materials with high Er concentration. This results in a record optical gain coefficient over 1500 dB/cm at 1536 nm band, at least larger by an order of magnitude than the previous gain record in Er materials. Leveraging this exceptional gain medium, we demonstrate room-temperature continuous-wave lasing operation by integrating with a photonic crystal microcavity, achieving a record-low threshold of 7 μW with the most compact size of any Er-based lasers. Furthermore, the unique Stark splitting characteristics of ErOCl provide optical gain in three wavelength bands and lead to lasing in these wavelengths by engineering the cavity. This is the first time that optical gain has been shown in three different wavelength bands in Er materials, together with the smallest size of laser cavity, could have many important applications in on-chip sensing and optical communication.

physics.app-ph↗

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation

Program safety (i.e., absence of undefined behaviors) is critical for correct operation of computer systems. It is usually verified at the source level (e.g., by separation logics) and preserved to the target by verified compilers (e.g., CompCert), thereby achieving end-to-end verification of safety. However, modern safe programming languages like Rust pose new problems in achieving end-to-end safety. Because not all functionalities can be implemented in the safe language, mixing safe and unsafe modules is needed. Therefore, verified compilation must preserve a modular notion of safety which can be composed at the target level. Furthermore, certain classes of errors (e.g., memory errors) are automatically excluded by verifying compilation (e.g., borrow checking) for modules written in safe languages. As a result, verified compilation needs to cooperate with verifying compilation to ensure end-to-end safety. To address the above problems, we propose a modular and generic definition of safety called open safety based on program semantics described as open labeled transition systems (LTS). Open safety is composable at the boundary of modules and can be modularly preserved by verified compositional compilation. Those properties enable separate verification of safety for heterogeneous modules and composition of the safety results at the target level. Open safety can be generalized to partial safety (i.e., only a certain class of errors can occur). By this we formalized the correctness of verifying compilation as derivation of total safety from partial safety. We demonstrate how our framework can combine verified and verifying compilation by developing a verified compiler for an ownership language (called Owlang) inspired by Rust. We evaluate our approach on the compositional safety verification using a hash map implemented by Owlang and C.

cs.PL↗

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules (Technical Report)

Verified compilation of open modules (i.e., modules whose functionality depends on other modules) provides a foundation for end-to-end verification of modular programs ubiquitous in contemporary software. However, despite intensive investigation in this topic for decades, the proposed approaches are still difficult to use in practice as they rely on assumptions about the internal working of compilers which make it difficult for external users to apply the verification results. We propose an approach to verified compositional compilation without such assumptions in the setting of verifying compilation of heterogeneous modules written in first-order languages supporting global memory and pointers. Our approach is based on the memory model of CompCert and a new discovery that a Kripke relation with a notion of memory protection can serve as a uniform and composable semantic interface for the compiler passes. By absorbing the rely-guarantee conditions on memory evolution for all compiler passes into this Kripke Memory Relation and by piggybacking requirements on compiler optimizations onto it, we get compositional correctness theorems for realistic optimizing compilers as refinements that directly relate native semantics of open modules and that are ignorant of intermediate compilation processes. Such direct refinements support all the compositionality and adequacy properties essential for verified compilation of open modules. We have applied this approach to the full compilation chain of CompCert with its Clight source language and demonstrated that our compiler correctness theorem is open to composition and intuitive to use with reduced verification complexity through end-to-end verification of non-trivial heterogeneous modules that may freely invoke each other (e.g., mutually recursively).

cs.PL↗

MVB: A Large-Scale Dataset for Baggage Re-Identification and Merged Siamese Networks

In this paper, we present a novel dataset named MVB (Multi View Baggage) for baggage ReID task which has some essential differences from person ReID. The features of MVB are three-fold. First, MVB is the first publicly released large-scale dataset that contains 4519 baggage identities and 22660 annotated baggage images as well as its surface material labels. Second, all baggage images are captured by specially-designed multi-view camera system to handle pose variation and occlusion, in order to obtain the 3D information of baggage surface as complete as possible. Third, MVB has remarkable inter-class similarity and intra-class dissimilarity, considering the fact that baggage might have very similar appearance while the data is collected in two real airport environments, where imaging factors varies significantly from each other. Moreover, we proposed a merged Siamese network as baseline model and evaluated its performance. Experiments and case study are conducted on MVB.

cs.CV↗