查看“用户:Hengfeng-Wei”的源代码
←
用户:Hengfeng-Wei
跳转至:
导航
、
搜索
因为以下原因,你没有权限编辑本页:
您所请求的操作仅限于这些用户组的用户使用:
管理员
、editor
您可以查看并复制此页面的源代码:
{{#css: #bodyContent { background-color: yellow; } body { background: navajowhite; } }} == Profile == Hengfeng Wei (魏恒峰) Contact: [mailto:hengxin0912@gmail.com 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. [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)] ---- Yesterday (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. 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, doi:10.1109/TPDS.2015.2453985 [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)] ---- 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". I am sorry to say that it is not right for us to conclude that VCC, in general, (i.e., VCC-SD in our terms) is NP-complete just because Pipelined-RAM is a weakening of causal consistency. However, I still believe that VCC-SD is NP-complete and that the basic idea of the polynomial reduction used in the NP-complete proof for VPC-SD will be useful in proving the NP-completeness of VCC-SD. The NP-complete proof for VPC-SD (along with VPC-MD) is credited to [http://www.nearly42.org/ Marzio De Biasi], the second author of this paper. ---- '''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 == - [http://hengxin.github.io/ hengxin@github.io]: A blog hosted on GitHub. - [http://stackexchange.com/users/2055160 hengxin@StackExchange]: My profile on StackExchange --- A wonderful Q/A site. - [https://github.com/hengxin hengxin@GitHub]: Open source projects. - [https://bitbucket.org/hengxin/ hengxin@Bitbucket]: Private repositories for unpublished papers and reports.
返回至
用户:Hengfeng-Wei
。
导航菜单
个人工具
登录
命名空间
用户页
讨论
变种
视图
阅读
查看源代码
查看历史
更多
搜索
导航
首页
最近更改
随机页面
帮助
工具
链入页面
相关更改
用户贡献
日志
特殊页面
页面信息