Xiaoxiao Yang (杨潇潇)                      

 

Associate Professor                   

State Key Laboratory of Computer Science                                

Institute of Software, Chinese Academy of Sciences                                                                                             

 

Email: xxyang@ios.ac.cn

 

 

Teaching

 

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)

 

 

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

    performance metrics.

 

   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

  successfully.

 

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

 

 

 

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.

 

2.  Modelling, Verification and Performance Evaluation of Concurrent Data

     Structures. Supported by Alexander von Humboldt Foundation.

 

3.  多核系统高性能并发数据结构算法分析与验证技术研究 Natural Science

     Foundation of Beijing,China 

 

 

 

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 25 May 2021