Xiaoxiao Yang

* *

Associate Professor

State Key Laboratory of Computer Science

Institute of Software, Chinese Academy of
Sciences

Email: xxyang@ios.ac.cn

(or xiaoxiaoyang1015@gmail.com)

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.
*T echnical Report No.
ISCAS-SKLCS-14-16.*

* Sep.
2014.*

__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 __

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
R____eport____ ____No.____ ISCAS-__

** SKLCS-15-13. Dec. 2015.**

* Linearizability via
Branching Bisimulation*

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*