Assistant Research Professor
State Key Laboratory of Computer Science
Institute of Software, Chinese Academy of Sciences
Spring semester 2013. The Art of Multiprocessor Programming. (for Graduates, University of Chinese Academy of Sciences)
The Art of Multiprocessor Programming. (for Graduates, Institute of
My research interests are program verification, concurrent data structures, multi-programming and concurrency theory.
My current research work is modelling, verification and performance evaluation of concurrent data structures.
2013.7-2015.9. Alexander von Humboldt Researcher in RWTH Aachen University. My host professor is Prof. Dr. Ir. Joost-Pieter Katoen.
2012.7- now. Assistant research professor. State Key Laboratory of Computer Science, ISCAS.
2009.6-2012.7. Postdoc researcher at ISCAS, headed by Prof. Huimin Lin.
2005-2009. PhD student in Xidian University, headed by Prof. Zhenhua Duan.
l Hao Wu, Xiaoxiao Yang and Joost-Pieter Katoen. Performance Evaluation of Concurrent Data Structures. SETTA 2016. LNCS 9984, pp. 38-49.
This paper reports the performance evaluation on several concurrent stacks, queues and lists.
Our analysis yields worst- and best-case bounds on performance metrics.
l Xiaoxiao Yang, Joost-Pieter Katoen, Huimin Lin and Hao Wu. Proving Linearizability via Branching Bisimulation. Technical report No. ISCAS-SKLCS-15-13. Dec. 2015.
In this paper, we conducted the experiment on 13 popular concurrent data structures yielding promising results,
including verifying linearizability for 13 algorithms, lock-free property for 8 algorithms, and revealing two bugs.
We have given the oral presentations about the result as follows:
(1) The myth of Linearization Points. A talk was given by Professor Huimin Lin (invited talk). SETTA 2015, Nanjing.
(2) Proving Linearizability and Progress Properties by Bisimulation. D-CON Workshop, 6. March, 2015. Germany.
(3) Proving Linearizability via Branching Bisimulation. A round-table meeting with Professor Leslie Lamport, 26. Oct. 2015. Beijing.
l Xiaoxiao Yang and Joost-Pieter Katoen. Proving Linearizability and Progress Properties by Bisimulation. Technical report No. ISCAS-SKLCS-14-16. Sep. 2014.
In this paper, we first proposed the idea using (divergence-sensitive) branching bisimulation to verify
linearizability as well as progress properties.
This idea using bisimulation started from my reading the stutter bisimulation in the book of “Principles
of Model Checking” (written by C. Baier and J. –P. Katoen) and the lecture “Concurrency Theory” given
by Prof. J. –P. Katoen in RWTH-Aachen University in 2013/2014. In the meanwhile, Prof. J. –P. suggested
to use the SCOOP tool (developed by Dr. Mark Timmer in University of Twente) to model the interleaved
executions of the Peterson Lock algorithm, Treiber’s lock-free stack, and HSY elimination stack.
These work inspired me to think deeply about the behavior equivalence between a concrete object and
an abstract object (specified by an atomic block), and motivated me to modify the definition of stutter
bisimulation to fit into the object implementation.
I first gave a definition that heavily relied on linearization points, by comparing the internal interleaved
transition between the concrete and abstract object systems. Then by the experiment, I found that
linearization points are not necessary to be involved, and modified it to a new definition, named co-bisimulation
(short for concurrent bisimulation). Afterwards, Prof. Huimin Lin told me that the definition is exactly the
branching bisimulation. Since then (Jul. 2014), I started the study on branching bisimulation
and concurrent data structures, and validating the idea in the paper by the future experiment.
An oral presentation about the work was first given at our group seminar at ISCAS (Beijing) on 20, Nov. 2014.
Before I returned to China in 2014, the experiment (based on CADP) on verifying linearizability and lock-free
property of Treiber concurrent stack and Michael-Scott lock-free queue had been finished successfully.
l Xiaoxiao Yang, Yu Zhang, Ming Fu and Xinyu Feng. A temporal programming model with atomic blocks based on projection temporal logic. Frontiers of Computer Science 8(6), pp. 958-976. 2014.
l Xiaoxiao Yang. Combining Separation Logic and Projection Temporal Logic to Reason about Non-blocking Concurrency. SOFL+MSVL 2014: 127-144.
TrComp was developed during 2015-2016 in our group (by Gaoang Liu). The purpose of this tool is to compute the branching bisimulation quotient
of a concurrent system by the higher-trace equivalence, which is a nice complement to the CADP toolset.
1. 基于非阻塞同步机制的多核并发系统模块化验证方法研究 National Natural Science Foundation of China NSFC No. 61100063 (2012.1-2014.12).
2. Modelling, Verification and Performance Evaluation of Concurrent Data Structures. Supported by Alexander von Humboldt Foundation (2013-2015).
I would like to thank the CADP group, particularly, Dr. Wenderlin Serwe and Prof. Hubert Garavel for their patience and support during our work.
Written by 2016.11.20