Source author record

Yanjing Wang

Yanjing Wang appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Catalog footprint

What is connected

12works
7topics
4close collaborators

Actions

Connect this record

Log in to claim

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

12 published item(s)

preprint2026arXiv

Cohet: A CXL-Driven Coherent Heterogeneous Computing Framework with Hardware-Calibrated Full-System Simulation

Conventional heterogeneous computing systems built on PCIe interconnects suffer from inefficient fine-grained host-device interactions and complex programming models. In recent years, many proprietary and open cache-coherent interconnect standards have emerged, among which compute express link (CXL) prevails in the open-standard domain after acquiring several competing solutions. Although CXL-based coherent heterogeneous computing holds the potential to fundamentally transform the collaborative computing mode of CPUs and XPUs, research in this direction remains hampered by the scarcity of available CXL-supported platforms, immature software/hardware ecosystems, and unclear application prospects. This paper presents Cohet, the first CXL-driven coherent heterogeneous computing framework. Cohet decouples the compute and memory resources to form unbiased CPU and XPU pools which share a single unified and coherent memory pool. It exposes a standard malloc/mmap interface to both CPU and XPU compute threads, leaving the OS dealing with smart memory allocation and management of heterogeneous resources. To facilitate Cohet research, we also present a full-system cycle-level simulator named SimCXL, which is capable of modeling all CXL sub-protocols and device types. SimCXL has been rigorously calibrated against a real CXL testbed with various CXL memory and accelerators, showing an average simulation error of 3%. Our evaluation reveals that CXL.cache reduces latency by 68% and increases bandwidth by 14.4x compared to DMA transfers at cacheline granularity. Building upon these insights, we demonstrate the benefits of Cohet with two killer apps, which are remote atomic operation (RAO) and remote procedure call (RPC). Compared to PCIe-NIC design, CXL-NIC achieves a 5.5 to 40.2x speedup for RAO offloading and an average speedup of 1.86x for RPC (de)serialization offloading.

preprint2026arXiv

CXL-DMSim: A Full-System CXL Disaggregated Memory Simulator With Comprehensive Silicon Validation

Compute eXpress Link (CXL) has emerged as a key enabler of memory disaggregation for future heterogeneous computing systems to expand memory on-demand and improve resource utilization. However, CXL is still in its infancy stage and lacks commodity products on the market, thus necessitating a reliable system-level simulation tool for research and development. In this paper, we propose CXL-DMSim, an open-source full-system simulator to simulate CXL disaggregated memory systems with high fidelity at a gem5-comparable simulation speed. CXL-DMSim incorporates a flexible CXL memory expander model along with its associated device driver, and CXL protocol support with CXL.io and CXL.mem. It can operate in both app-managed mode and kernel-managed mode, with the latter using a dedicated NUMA-compatible mechanism. The simulator has been rigorously verified against a real hardware testbed with both FPGAand ASIC-based CXL memory devices, which demonstrates the qualification of CXL-DMSim in simulating the characteristics of various CXL memory devices at an average simulation error of 3.4%. The experimental results using LMbench and STREAM benchmarks suggest that the CXL-FPGA memory exhibits a ~2.88x higher latency than local DDR while the CXL-ASIC latency is ~2.18x; CXL-FPGA achieves 45-69% of local DDR memory bandwidth, whereas the number for CXLASIC is 82-83%. The study also reveals that CXL memory can significantly enhance the performance of memory-intensive applications, improved by 23x at most with limited local memory for Viper key-value database and approximately 60% in memorybandwidth-sensitive scenarios such as MERCI. Moreover, the simulator's observability and expandability are showcased with detailed case-studies, highlighting its great potential for research on future CXL-interconnected hybrid memory pool.

preprint2022arXiv

An Epistemic Interpretation of Tensor Disjunction

This paper aims to give an epistemic interpretation to the tensor disjunction in dependence logic, through a rather surprising connection to the so-called weak disjunction in Medvedev's early work on intermediate logic under the Brouwer-Heyting-Kolmogorov (BHK)-interpretation. We expose this connection in the setting of inquisitive logic with tensor disjunction discussed by Ciardelli and Barbero (2019}, but from an epistemic perspective. More specifically, we translate the propositional formulae of inquisitive logic with tensor into modal formulae in a powerful epistemic language of "knowing how" following the proposal by Wang (2021). We give a complete axiomatization of the logic of our full language based on Fine's axiomatization of S5 modal logic with propositional quantifiers. Finally, we generalize the tensor operator with parameters $k$ and $n$, which intuitively captures the epistemic situation that one knows $n$ potential answers to $n$ questions and is sure $k$ answers of them must be correct. The original tensor disjunction is the special case when $k=1$ and $n=2$. We show that the generalized tensor operators do not increase the expressive power of our logic, the inquisitive logic, and propositional dependence logic, though most of these generalized tensors are not uniformly definable in these logics, except in our dynamic epistemic logic of knowing how.

preprint2022arXiv

Are Bundles Good Deals for FOML?

Bundled products are often offered as good deals to customers. When we bundle quantifiers and modalities together (as in $\exists x \Box$, $\Diamond \forall x$ etc.) in first-order modal logic (FOML), we get new logical operators whose combinations produce interesting fragments of FOML without any restriction on the arity of predicates, the number of variables, or the modal scope. It is well-known that finding decidable fragments of FOML is hard, so we may ask: do bundled fragments that exploit the distinct expressivity of FOML constitute good deals in balancing the expressivity and complexity? There are a few positive earlier results on some particular fragments. In this paper, we try to fully map the terrain of bundled fragments of FOML in (un)decidability, and in the cases without a definite answer yet, we show that they lack the finite model property. Moreover, whether the logics are interpreted over constant domains (across states/worlds) or increasing domains presents another layer of complexity. We also present the \textit{loosely bundled fragment}, which generalizes the bundles and yet retain decidability (over increasing domain models).

preprint2022arXiv

Inquisitive Logic as an Epistemic Logic of Knowing How

In this paper, we present an alternative interpretation of propositional inquisitive logic as an epistemic logic of knowing how. In our setting, an inquisitive logic formula $α$ being supported by a state is formalized as "knowing how to resolve $α$" (more colloquially, "knowing how $α$ is true") holds on the S5 epistemic model corresponding to the state. Based on this epistemic interpretation, we use a dynamic epistemic logic with both know-how and know-that operators to capture the epistemic information behind the innocent-looking connectives in inquisitive logic. We show that the set of valid know-how formulas corresponds precisely to the inquisitive logic. The main result is a complete axiomatization with intuitive axioms using the full dynamic epistemic language. Moreover, we show that the know-how operator and the dynamic operator can both be eliminated without changing the expressivity over models, which is consistent with the modal translation of inquisitive logic existing in the literature. We hope our framework can give an intuitive alternative interpretation of various concepts and technical results in inquisitive logic, and also provide a powerful and flexible tool to do inquisitive reasoning in an epistemic context.

preprint2016arXiv

"Knowing value" logic as a normal modal logic

Recent years witness a growing interest in nonstandard epistemic logics of "knowing whether", "knowing what", "knowing how", and so on. These logics are usually not normal, i.e., the standard axioms and reasoning rules for modal logic may be invalid. In this paper, we show that the conditional "knowing value" logic proposed by Wang and Fan \cite{WF13} can be viewed as a disguised normal modal logic by treating the negation of the Kv operator as a special diamond. Under this perspective, it turns out that the original first-order Kripke semantics can be greatly simplified by introducing a ternary relation $R_i^c$ in standard Kripke models, which associates one world with two $i$-accessible worlds that do not agree on the value of constant $c$. Under intuitive constraints, the modal logic based on such Kripke models is exactly the one studied by Wang and Fan (2013,2014}. Moreover, there is a very natural binary generalization of the "knowing value" diamond, which, surprisingly, does not increase the expressive power of the logic. The resulting logic with the binary diamond has a transparent normal modal system, which sharpens our understanding of the "knowing value" logic and simplifies some previously hard problems.

preprint2016arXiv

A Dynamic Epistemic Framework for Conformant Planning

In this paper, we introduce a lightweight dynamic epistemic logical framework for automated planning under initial uncertainty. We reduce plan verification and conformant planning to model checking problems of our logic. We show that the model checking problem of the iteration-free fragment is PSPACE-complete. By using two non-standard (but equivalent) semantics, we give novel model checking algorithms to the full language and the iteration-free language.

preprint2016arXiv

Beyond knowing that: a new generation of epistemic logics

Epistemic logic has become a major field of philosophical logic ever since the groundbreaking work by Hintikka (1962). Despite its various successful applications in theoretical computer science, AI, and game theory, the technical development of the field has been mainly focusing on the propositional part, i.e., the propositional modal logics of "knowing that". However, knowledge is expressed in everyday life by using various other locutions such as "knowing whether", "knowing what", "knowing how" and so on (knowing-wh hereafter). Such knowledge expressions are better captured in quantified epistemic logic, as was already discussed by Hintikka (1962) and his sequel works at length. This paper aims to draw the attention back again to such a fascinating but largely neglected topic. We first survey what Hintikka and others did in the literature of quantified epistemic logic, and then advocate a new quantifier-free approach to study the epistemic logics of knowing-wh, which we believe can balance expressivity and complexity, and capture the essential reasoning patterns about knowing-wh. We survey our recent line of work on the epistemic logics of "knowing whether", "knowing what" and "knowing how" to demonstrate the use of this new approach.

preprint2015arXiv

A Logic of Knowing How

In this paper, we propose a single-agent modal logic framework for reasoning about goal-direct "knowing how" based on ideas from linguistics, philosophy, modal logic and automated planning. We first define a modal language to express "I know how to guarantee phi given psi" with a semantics not based on standard epistemic models but labelled transition systems that represent the agent's knowledge of his own abilities. A sound and complete proof system is given to capture the valid reasoning patterns about "knowing how" where the most important axiom suggests its compositional nature.

preprint2015arXiv

From rules to runs: A dynamic epistemic take on imperfect information games

In the literature of game theory, the information sets of extensive form games have different interpretations, which may lead to confusions and paradoxical cases. We argue that the problem lies in the mix-up of two interpretations of the extensive form game structures: game rules or game runs which do not always coincide. In this paper, we try to separate and connect these two views by proposing a dynamic epistemic framework in which we can compute the runs step by step from the game rules plus the given assumptions of the players. We propose a modal logic to describe players' knowledge and its change during the plays, and provide a complete axiomatization. We also show that, under certain conditions, the mix-up of the rules and the runs is not harmful due to the structural similarity of the two.

preprint2013arXiv

Knowing Whether

Knowing whether a proposition is true means knowing that it is true or knowing that it is false. In this paper, we study logics with a modal operator Kw for knowing whether but without a modal operator K for knowing that. This logic is not a normal modal logic, because we do not have Kw (phi -> psi) -> (Kw phi -> Kw psi). Knowing whether logic cannot define many common frame properties, and its expressive power less than that of basic modal logic over classes of models without reflexivity. These features make axiomatizing knowing whether logics non-trivial. We axiomatize knowing whether logic over various frame classes. We also present an extension of knowing whether logic with public announcement operators and we give corresponding reduction axioms for that. We compare our work in detail to two recent similar proposals.