“用户:Hengfeng-Wei”的版本间的差异
来自Algorithm Wiki
Hengfeng-Wei（讨论 | 贡献） （→Publications： using "mw-collapsible"） |
Hengfeng-Wei（讨论 | 贡献） （→Publications： default: mw-collapsed） |
||
| 第18行： | 第18行： | ||
# [[#Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas | Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas]] | # [[#Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas | Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas]] | ||
# [[#Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context | Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context]] | # [[#Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context | Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context]] | ||
| + | |||
| + | ---- | ||
| + | ---- | ||
=== Probabilistically-Atomic 2-Atomicity: Enabling Almost Strong Consistency in Distributed Storage Systems === | === Probabilistically-Atomic 2-Atomicity: Enabling Almost Strong Consistency in Distributed Storage Systems === | ||
| 第26行： | 第29行： | ||
[https://www.computer.org/csdl/trans/tc/preprint/07547362-abs.html abstract@IEEE] [https://arxiv.org/abs/1507.01663 pdf@arXiv (not up-to-date)] | [https://www.computer.org/csdl/trans/tc/preprint/07547362-abs.html abstract@IEEE] [https://arxiv.org/abs/1507.01663 pdf@arXiv (not up-to-date)] | ||
| − | <div class="mw-collapsible"> | + | <div class="mw-collapsible mw-collapsed"> |
Last night (2016-10-13), I reread the paper [http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#interprocess "On Interprocess Communication --- Part II: Algorithms"] of Leslie Lamport, and found 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. | Last night (2016-10-13), I reread the paper [http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#interprocess "On Interprocess Communication --- Part II: Algorithms"] of Leslie Lamport, and found 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. | ||
| 第47行： | 第50行： | ||
[https://www.computer.org/csdl/trans/td/2016/05/07152941.pdf pdf@IEEE] [https://arxiv.org/pdf/1302.5161.pdf pdf@arXiv(not up-to-date)] | [https://www.computer.org/csdl/trans/td/2016/05/07152941.pdf pdf@IEEE] [https://arxiv.org/pdf/1302.5161.pdf pdf@arXiv(not up-to-date)] | ||
| − | <div class="mw-collapsible"> | + | <div class="mw-collapsible mw-collapsed"> |
In the Conclusion section, we discussed the VCC (Verifying [http://link.springer.com/article/10.1007/BF01784241 Causal Consistency]) problem and wrote: "Because Pipelined-RAM is a weakening of causal consistency, our NP-complete result also applies to the general problem of verifying causal consistency". | In the Conclusion section, we discussed the VCC (Verifying [http://link.springer.com/article/10.1007/BF01784241 Causal Consistency]) problem and wrote: "Because Pipelined-RAM is a weakening of causal consistency, our NP-complete result also applies to the general problem of verifying causal consistency". | ||
2016年10月14日 (五) 10:16的版本
Profile
Hengfeng Wei (魏恒峰)
Contact: hengxin0912@gmail.com
Researches
I am interested in Distributed Computing Theory and Formal Methods.
Publications
- Probabilistically-Atomic 2-Atomicity: Enabling Almost Strong Consistency in Distributed Storage Systems
- Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas
- Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context
Probabilistically-Atomic 2-Atomicity: Enabling Almost Strong Consistency in Distributed Storage Systems
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. abstract@IEEE pdf@arXiv (not up-to-date)
[展开]
Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas
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, doi:10.1109/TPDS.2015.2453985 pdf@IEEE pdf@arXiv(not up-to-date)
[展开]
Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context
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.
