用户:Hengfeng-Wei

Profile

Hengfeng Wei (魏恒峰)

Contact: hengxin0912@gmail.com

Researches

I am interested in Distributed Computing Theory and Formal Methods.

Publications

 Hengfeng Wei, Yu Huang, Jian Lu. 
 Probabilistically-Atomic 2-Atomicity: Enabling Almost Strong Consistency in Distributed Storage Systems. 
 In IEEE Trans. Comput., xx(x):x--x , PrePrints, doi:10.1109/TC.2016.2601322, 2016.

---

Later, I reread the paper "On Interprocess Communication --- Part II: Algorithms" of Leslie Lamport, and find that in Proposition 5, Lamport has proved that in the single-writer model a regular register is atomic if two successive reads that overlap the same write cannot obtain the new then the old value. The phenomenon that "two successive reads that overlap the same write cannot obtain the new then the old value" is exactly the old-new inversion anomaly. Therefore, Lamport has shown that a regular register is atomic if it does not allow old-new inversion anomalies. This is very similar to Theorem 1 in our paper which essentially states that the PA2AM algorithm implements a 2-atomic register and the old-new inversion anomaly is the only cause of atomicity violation.

The major difference between Proposition 5 of Lamport and Theorem 1 in our paper is that Proposition 5 is at the specification level while Theorem 1 is at the implementation level.

Combining Proposition 5 and Theorem 1, we obtain

Conjecture 1

In the single-writer model, 2-atomicity is equivalent to regularity.

Conjecture 2

In the single-write model, PA2AM implements a regular register.

---

 Hengfeng Wei, Marzio De Biasi, Yu Huang, Jiannong Cao, and Jian Lu. 
 Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas.
 In IEEE Trans. Parallel Distrib. Syst., 27(5):1511--1523, 2016.

 Hengfeng Wei, Yu Huang, Jiannong Cao, Xiaoxing Ma, Jian Lu. 
 Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context. 
 In Proceedings of the 10th IEEE International Conference on Pervasive Computing and Communications 
 (IEEE PerCom '12), pages 30--38, 2012.

Links

- hengxin@github.io: A blog hosted on GitHub.

- hengxin@StackExchange: My profile on StackExchange --- A wonderful Q/A site.

- hengxin@GitHub: Open source projects.

- hengxin@Bitbucket: Private repositories for unpublished papers and reports.