Xiaoxiao Yang (杨潇潇)
State Key Laboratory of Computer Science
Institute of Software, Chinese Academy of Sciences
Spring semester 2013-until now. The Art of Multiprocessor Programming.
(for Graduates, University of Chinese Academy of Sciences)
Seminar 2011/2012. The Art of Multiprocessor Programming.
(for Graduates, Institute of Software, CAS)
My research interests are formal methods, verification, concurrent algorithms and
data structures, multi-programming.
My current research work is the design, verification and performance evaluation of
concurrent data structures.
2020.9-until now: Associate Professor, State Key Laboratory of Computer Science, ISCAS.
2013.7-2015.9: Alexander von Humboldt Researcher in RWTH Aachen University. My host professor is Prof. Dr. Dr. Ir. Joost-Pieter Katoen.
2012.7- 2020.9: Assistant professor, State Key Laboratory of Computer Science, ISCAS.
2009.7-2012.7: Postdoc researcher at ISCAS, headed by Prof. Huimin Lin.
2005.9 - 2009.6: PhD student in Xidian University, headed by Prof. Zhenhua Duan.
The Key Publications (selected)
• Xiaoxiao Yang, Joost-Pieter Katoen, Huimin Lin and Hao Wu. Branching Bisimulation and Concurrent Object Verification. The 48th IEEE/IFIP
International Conference on Dependable Systems and Networks (DSN’18). Luxembourg. June 24-28, 2018.
• 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
• Xiaoxiao Yang, Joost-Pieter Katoen, Huimin Lin and Hao Wu. Proving Linearizability via Branching Bisimulation. Technical Report No. ISCAS-
SKLCS-15-13. Dec. 2015. (Online TR: Proving Linearizability via Branching Bisimulation. CoRR abs/1609.07546, 2016)
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.
• Xiaoxiao Yang and Joost-Pieter Katoen. Proving Linearizability and Progress Properties by Bisimulation. Technical Report No. ISCAS-SKLCS-14-16. Sep.
2014. (Online TR: Verifying Concurrent Stacks by Divergence-Sensitive Bisimulation. CoRR abs/1701.06104, 2017)
This online technical report is Cited by POPL’2019, POPL’2020 etc.
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 Joost–Pieter Katoen)
and the lecture “Concurrency Theory” given by Prof. Joost–Pieter Katoen in
RWTH Aachen University in 2013/2014. In the meanwhile, he suggested me 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 found a link between stutter
bisimulation and the concurrent object implementation. Further, I tried 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 more experiments.
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
• 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.
• Xiaoxiao Yang. Combining Separation Logic and Projection Temporal Logic to Reason about Non-blocking Concurrency. SOFL+MSVL 2014: 127-144.
• Xiaoxiao Yang, Yu Zhang, Ming Fu and Xinyu Feng. A Concurrent Temporal Programming Model with Atomic Blocks. ICFEM 2012. Springer-Verlag.
LNCS7635: 22-37. 2012.
• Xiaoxiao Yang, Zhenhua Duan and Qian Ma. Axiomatic Semantics of Projection Temporal Logic Programs. 2010.
Mathematical Structures in Computer Science.
Cambridge University Press. Vol. 20 (5): 865-914. 2010
• Xiaoxiao Yang and Zhenhua Duan. Operational Semantics of Framed Tempura.
Journal of Logic and Algebraic Programming. Elsevier. Vol. 78(1): 22-51. 2008.
• Zhenhua Duan, Xiaoxiao Yang and Maciej Koutny. Framed Temporal Logic Programming. Science of Computer Programming.
Elsevier. Vol.70 (1): 31-61. 2008 (cited by 107)
• Zhenhua Duan, Xiaoxiao Yang and Maciej Koutny. Semantics of Framed Temporal Logic Programs. The 21st International Conference on Logic
Programming (ICLP’05). LNCS3668. 2005: 356-370. Springer-Verlag.
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.
2. Modelling, Verification and Performance Evaluation of Concurrent Data
Structures. Supported by Alexander von Humboldt Foundation.
3. 多核系统高性能并发数据结构算法分析与验证技术研究 Natural Science
Foundation of Beijing,China
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 25 May 2021