Welcome to Xiaoxiao Yang's Homepage!

Xiaoxiao Yang

Associate Professor

State Key Laboratory of Computer Science

Institute of Software, Chinese Academy of Sciences

Teaching

In our lab, I first introduced and organized the course on “The Art of Multiprocessor Programming” in 2011. And opened the course in UCAS in 2013.

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, SKLCS, Institute of Software, CAS)

Research Interests

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.

Experience

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, with 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, Hao Wu and Gaoang Liu.

Branching Bisimulation and Concurrent Object Verification. The 48th IEEE/IFIP

International Conference on Dependable Systems and Networks (DSN’18).

Luxembourg. June 24-28, 2018.

Related Versions of DSN’18:

1. TR No. ISCAS-SKLCS-14-16.

2. TR No. ISCAS-SKLCS-15-13.

• Xiaoxiao Yang and Joost-Pieter Katoen. Proving Linearizability and Progress of

Concurrent Objects 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. The idea using bisimulation started from my reading the stutter bisimulation introduced in the book “Principles of Model Checking” (written by C. Baier and J. -P. Katoen) and attending the lecture “Concurrency Theory” (given by Thomas Noll and Joost-Pieter Katoen) in RWTH Aachen University in 2013. In the meanwhile, Joost-Pieter suggested using the SCOOP tool (developed by Dr. Mark Timmer in University of Twente) to model the Peterson Lock, the Treiber’s lock-free stack and the HSY elimination stack. These inspired me to think deeply about the behavior equivalence between a concrete object and an abstract object (specified by a single atomic block).

I ruled out the trace equivalence and simulation equivalence due to the absence of divergence, and found that there may exist some connection between (divergence-sensitive) stutter bisimulation and the concurrent object implementation. After that,

I tried to give a variant of stutter bisimulation to fit into the object implementation. I first gave a definition that heavily relied on linearization points (LPs), by comparing the internal interleaved transitions between the concrete and abstract object systems. Then I found a simpler structure that does not need LPs in the definition, and modified it to a new definition, named co-bisiumulation (short for concurrent bisimulation).

Although it was unknown, at that time, whether there was a natural equivalence relation between abstract object systems and concrete object systems, I believed that it is a correct definition suitable for analyzing and verifying object programs.

In January 2014, the idea to explore an inherent equivalence relation that preserves both linearizability and progress properties between abstract and concrete object systems was finished and the corresponding verification methods were established.

The initial version of the idea (See: TR No. ISCAS-SKLCS-14-16) was submitted to CONCUR’14 and POPL’14 respectively. Some helpful comments were given by the reviewers. One reviewer from CONCUR’14 reminded that the co-bisimulation

seemed to be the branching bisimulation. Almost all reviewers of POPL’14 suggested to do experiments to validate the idea. In addition, before the submission of POPL’14, I invited Prof. Huimin Lin to give some opinions on the manuscript, he also reminded that the co-bisimulation in the paper is the branching bisimulation.

Since then (July 2014), I started to read the classic paper on branching bisimulation (Glabbeek&Weijland’96). And with the existing bisimulation techniques and tools, I

conducted experiments to prove the correctness of concurrent objects.

Before I returned to Beijing for a short vacation (in Nov. 2014), the experiment on verifying linearizability and lock-free property of Treiber’s concurrent stack and Michael-Scott lock-free queue had been finished successfully. In particular, Michael-Scott lock-free queue was the first algorithm with Non-Fixed Linearization Points I verified.

On 20 Nov. 2014, I was invited to give a talk at the ISCAS group seminar in Beijing. It was the first time to show my unpublished work (i.e., Technical Report No. ISCAS-SKLCS-14-16). I introduced the details of my work including the motivation, results and verification methods, and demonstrated the whole experiments on the Treiber’s stack and the MS queue to the audience.

When I went back to Germany in Dec. 2014, we continued to study more algorithms. Until Feb. 2015, all experiments on modeling and verifying concurrent data structures were finished in RWTH Aachen University (in Aachen, Germany), which validated

the effectiveness and efficiency of our methods.

From these experiments, I also found a new and interesting thing, that is: All the algorithms seemed to show that the state changes saved in the quotient system were exactly the LPs of object algorithms. The next question I had to face was that: how to prove this finding was a general result for any concurrent objects.

I tried to give a constructive proof based on colored traces (a trace characterization of branching bisimulation), but it failed through lack of a formal definition of LPs.

Huimin Lin suggested using the K-trace (another equivalent characterization defined in [Glabbeek&Weijland’96]) since it is an inductive definition that perhaps made the proof easier. But it was still hard to prove a property of LPs without its definition.

As an example, I applied the K-trace to analyzing LPs of Herlihy-Wing queue, where I showed that there existed an LP of which the state change is 1-trace equivalence (i.e., ordinary trace equivalence), but not 2-trace (i.e., branch) equivalence.

The extended version with all experiments was submitted to POPL’15. In this version, LPs were formally defined using the branching bisimulation equivalence. However, I sometimes doubted the definition, that is, why the “take effect” in linearizability was the same as the “take effect” in branching bisimulation.

The reviewers of POPL’15 gave a lot of comments on LPs. Some were helpful and enlightening, and some were incorrect. With these comments of POPL’15, I understood the non-fixed LPs more deeply, and meanwhile, I realized that not all transitions in the quotient were LPs, although these state changes (not LPs) were also essential in locating LPs in theorem proofs. I continued my research on the issue of effects. This research was finished in Dec. 2017 (Technical Report No. ISCAS-SKLCS-17-06), and the original idea proposed in 2014 was accepted by DSN’18.

• 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 results in the manuscripts

TR No. SCAS-SKLCS-14-16 and TR No.SKLCS-15-13 as follows:

(1) Proving Linearizability and Progress Properties by Bisimulation. A talk (given by Xiaoxiao Yang) on D-CON Workshop, 6. March, 2015. Germany.

(2) Proving Linearizability via Branching Bisimulation. A round-table meeting with

Professor Leslie Lamport, 26. Oct. 2015. Beijing.

(3) The myth of Linearization Points. A talk was given by Prof. Huimin Lin, Keynote speaker. SETTA 2015, Nanjing.

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

• 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

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

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 complement to the CADP toolset.

Project

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

Acknowledgement

Thank Humboldt Foundation and my host professor Joost-Pieter Katoen who gave me support and freedom to try new research areas.

Many thanks to the CADP group, particularly, Dr. Wenderlin Serwe and Prof. Hubert Garavel for their patience and support during the experiments.

Written by 6 August 2022