Xiaoxiao Yang                       

 

Assistant Research Professor                   

State Key Laboratory of Computer Science

Institute of Software, Chinese Academy of Sciences    

 

Email: xxyang@ios.ac.cn

 

 

Teaching

 

Spring semester 2013. 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)

 

Research Interests

 

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.

 

 

Experience

 

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.  

 

 

Publications (selected)

 

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.

 

 

Tool

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. 

 

 

Project

 

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).

 

 

 

Acknowledgement

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