“用户:Hengfeng-Wei”的版本间的差异

2021年1月13日 (三) 10:21的最新版本

Profile

                                               Please Move to MY NEW HOMEPAGE

Hengfeng Wei (魏恒峰)

Research Assistant (助理研究员)：From 2017-01

 Software Institute                                      (软件学院)
 State Key Laboratory for Novel Software Technology      (软件新技术国家重点实验室)
 Nanjing University （Gulou Campus）                     (南京大学 鼓楼校区)
 Office: 926                                             (费彝民楼)

 Addr: 163 Xianlin Road, Qixia District, Nanjing, Jiangsu 210023, China     (江苏省南京市栖霞区仙林大道163号南京大学仙林校区 210023)

 Email:

Research Interests

I am interested in Distributed Computing Theory and Formal Methods.

Publications

dblp: Hengfeng Wei

scholar: Hengfeng Wei

[PA@TPDS2020]: Achieving Probabilistic Atomicity with Well-Bounded Staleness and Low Read Latency in Distributed Datastores
[RefineJupiter@JCST2020]: Jupiter Made Abstract, and Then Refined
[SpecFramework@SRDS2020]: Specification Framework for Weakly Consistent Replicated Data Types (WIP)
[FastAtomic@PODC2020]: Fine-grained Analysis on Fast Implementations of Multi-writer Atomic Registers of Multi-writer Atomic Registers
[PaxosStore@软件学报2020] PaxosStore中共识算法TPaxos的推导、规约与精化
[CRDT@软件学报2020] CRDT协议的TLA+ 描述与验证

---

[Jupiter@OPODIS2018@PODC-BA2018]: Specification and Implementation of Replicated List: The Jupiter Protocol Revisited

---

[RVSI@SRDS2017]: Parameterized and Runtime-tunable Snapshot Isolation in Distributed Transactional Key-value Stores
[PA2AM@TC2017]: Probabilistically-Atomic 2-Atomicity: Enabling Almost Strong Consistency in Distributed Storage Systems

---

[VPC@TPDS2016]: Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas
[CTL3@PerCom2012]: Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context

Achieving Probabilistic Atomicity with Well-Bounded Staleness and Low Read Latency in Distributed Datastores

 Lingzhi Ouyang, Yu Huang, Hengfeng Wei, Jian Lu
 IEEE Trans. on Parallel and Distributed Systems, accepted, Nov. 2020.

Jupiter Made Abstract, and Then Refined

 Hengfeng Wei, Ruize Tang, Yu Huang, Jian Lu. 
 “Jupiter Made Abstract, and then Refined”.
 Journal of Computer Science and Technology, accepted, Aug. 2020.

A Generic Specification Framework for Weakly Consistent Replicated Data Types

 Xue Jiang, Hengfeng Wei, Yu Huang.
 “A Generic Specification Framework for Weakly Consistent Replicated Data Types”.
 In Proceedings of the 39th International Symposium on Reliable Distributed Systems (SRDS 2020). Accepted. (To Appear).

Fine-grained Analysis on Fast Implementations of Multi-writer Atomic Registers of Multi-writer Atomic Registers

 Kaile Huang, Yu Huang, and Hengfeng Wei. 
 “Fine-grained Analysis on Fast Implementations of Multi-writer Atomic Registers of Multi-writer Atomic Registers”.
 In Proceedings of the ACM Symposium on Principles of Distributed Computing (PODC 2020), 2020.

PaxosStore中共识算法TPaxos的推导、规约与精化

 易星辰, 魏恒峰, 黄宇, 乔磊, 吕建. 
 PaxosStore中共识算法TPaxos的推导、规约与精化. 
 软件学报 2020. 2020年第8期.

CRDT协议的TLA+ 描述与验证

 易星辰, 魏恒峰, 黄宇, 吕建. 
 CRDT协议的TLA+ 描述与验证.
 软件学报 2020. 2020年第6期.

Specification and Implementation of Replicated List: The Jupiter Protocol Revisited

 Hengfeng Wei, Yu Huang, and Jian Lu.
 “Specification and Implementation of Replicated List: The Jupiter Protocol Revisited”. 
 In: 22nd International Conference on Principles of Distributed Systems, OPODIS 2018, December 17-19, 2018, Hong Kong, China.
 2018, 12:1–12:16. url: https://doi.org/10.4230/LIPIcs.OPODIS.2018.12

 Hengfeng Wei, Yu Huang, and Jian Lu.
 “Brief Announcement: Specification and Implementation of Replicated List: The Jupiter Protocol Revisited”.
 In: Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing. PODC ’18.
 Egham, United Kingdom: ACM, 2018, pp. 81–83. url: http://doi.acm.org/10.1145/3212734.3212

 Paper: Jupiter@PODC-BA'2018  Paper: Jupiter@OPODIS'2018  [Paper: Jupiter@arXiv (full version)]

This work is inspired by the work on "Specification and Complexity of Collaborative Text Editing" published in PODC'2016 by Hagit Attiya et al.

Parameterized and Runtime-tunable Snapshot Isolation in Distributed Transactional Key-value Stores

 Hengfeng Wei, Yu Huang, Jian Lu.
 Parameterized and Runtime-tunable Snapshot Isolation in Distributed Transactional Key-value Stores.
 In Proc. of the 36th International Symposium on Reliable Distributed Systems (SRDS), pp. 21--33, Hong Kong, China, Sep.2017.
 [Paper:RVSI@SRDS17]

The formal specification of RVSI (Relaxed Version Snapshot Isolation) in this work is partly inspired by the work on "Relaxed Currency Serializability for Middle-Tier Caching and Replication" published in SIGMOD'2006 by Philip A.Bernstein et al.

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. (IEEE Transactions on Computers), 66(3):502--514, doi:10.1109/TC.2016.2601322, March 2017.
 [abstract@IEEE]  [Paper: PA2AM@TC'2017] [Paper: PA2AM@arXiv (not up-to-date)]

Last night (2016-10-13), I reread the paper "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.

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, May 2016, doi:10.1109/TPDS.2015.2453985
 [abstract@IEEE]  [Paper: VPC@TPDS'2016] [Paper: VPC@arXiv(not up-to-date)]
 SCI: DJ5HS

In the Conclusion section, we discussed the VCC (Verifying 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 think 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-completeness proof for VPC-SD (along with VPC-MD) is mainly credited to Marzio De Biasi, the second author of this paper.

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.
 [abstract@IEEE]  [Paper: CTL3@PerCom'2012]
 EI: 20122315082503

Projects

Links

hengxin@GitHub

hengxin@StackExchange

@@ 第8行： / 第8行： @@
 [[File:Whf-white-2016-12.jpg|right|90px]]
-Hengfeng Wei (魏恒峰)     [[Media:Weihengfeng-cv-en.pdf | cv (en)]]      [[Media:Weihengfeng-cv-ch.pdf | cv (ch)]]
+                                                '''<big><big><big><big><big>Please Move to [https://hengxin.github.io/ MY NEW HOMEPAGE]</big></big></big></big></big>'''
+Hengfeng Wei (魏恒峰)
 * Research Assistant (助理研究员)：From 2017-01
-   Institute of Computer Software                          (软件所)
+   Software Institute                                      (软件学院)
    State Key Laboratory for Novel Software Technology      (软件新技术国家重点实验室)
-   Department of Computer Science and Technology           (计算机科学与技术系)
+   Nanjing University （Gulou Campus）                     (南京大学 鼓楼校区)
-   Nanjing University                                      (南京大学)
+   Office: 926                                             (费彝民楼)
-   Addr: 163 Xianlin Road, Nanjing 210023, P. R. China     (江苏省南京市栖霞区仙林大道163号南京大学仙林校区 210023)
+   Addr: 163 Xianlin Road, Qixia District, Nanjing, Jiangsu 210023, China     (江苏省南京市栖霞区仙林大道163号南京大学仙林校区 210023)
-  Office: 302
-  Mailbox: H016
    Email: [[File:Hfwei-njumail.png | hfwei-nju-edu-cn]]
@@ 第28行： / 第29行： @@
 == Publications ==
-[http://dblp.uni-trier.de/pers/hd/w/Wei:Hengfeng dblp: Hengfeng Wei] [https://scholar.google.com/citations?user=HK9-98EAAAAJ&hl=en scholar: Hengfeng Wei]
+[http://dblp.uni-trier.de/pers/hd/w/Wei:Hengfeng dblp: Hengfeng Wei]
-* [[#AOT | AOT: Algebraic Operational Transformation (WIP)]]
+[https://scholar.google.com/citations?user=HK9-98EAAAAJ&hl=en scholar: Hengfeng Wei]
-* [[#JCSS | JCSS: CSS for Jupiter]]
-* [[#Parameterized and Runtime-tunable Snapshot Isolation in Distributed Transactional Key-value Stores | RVSI: Parameterized and Runtime-tunable Snapshot Isolation in Distributed Transactional Key-value Stores]]
+* [[#Achieving Probabilistic Atomicity with Well-Bounded Staleness and Low Read Latency in Distributed Datastores | [PA@TPDS2020]: Achieving Probabilistic Atomicity with Well-Bounded Staleness and Low Read Latency in Distributed Datastores]]
-* [[#Probabilistically-Atomic 2-Atomicity: Enabling Almost Strong Consistency in Distributed Storage Systems | PA2AM: Probabilistically-Atomic 2-Atomicity: Enabling Almost Strong Consistency in Distributed Storage Systems]]
+* [[#Jupiter Made Abstract, and Then Refined | [RefineJupiter@JCST2020]: Jupiter Made Abstract, and Then Refined]]
-* [[#Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas | VPC: Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas]]
+* [[#A Generic Specification Framework for Weakly Consistent Replicated Data Types | [SpecFramework@SRDS2020]: Specification Framework for Weakly Consistent Replicated Data Types (WIP)]]
-* [[#Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context | CTL3: Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context]]
+* [[#Fine-grained Analysis on Fast Implementations of Multi-writer Atomic Registers of Multi-writer Atomic Registers | [FastAtomic@PODC2020]: Fine-grained Analysis on Fast Implementations of Multi-writer Atomic Registers of Multi-writer Atomic Registers]]
+* [[#PaxosStore中共识算法TPaxos的推导、规约与精化 | [PaxosStore@软件学报2020] PaxosStore中共识算法TPaxos的推导、规约与精化]]
+* [[#CRDT协议的TLA+ 描述与验证 | [CRDT@软件学报2020] CRDT协议的TLA+ 描述与验证]]
+---
+* [[#Specification and Implementation of Replicated List: The Jupiter Protocol Revisited | [Jupiter@OPODIS2018@PODC-BA2018]: Specification and Implementation of Replicated List: The Jupiter Protocol Revisited]]
+---
+* [[#Parameterized and Runtime-tunable Snapshot Isolation in Distributed Transactional Key-value Stores | [RVSI@SRDS2017]: Parameterized and Runtime-tunable Snapshot Isolation in Distributed Transactional Key-value Stores]]
+* [[#Probabilistically-Atomic 2-Atomicity: Enabling Almost Strong Consistency in Distributed Storage Systems | [PA2AM@TC2017]: Probabilistically-Atomic 2-Atomicity: Enabling Almost Strong Consistency in Distributed Storage Systems]]
+---
+* [[#Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas | [VPC@TPDS2016]: Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas]]
+* [[#Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context | [CTL3@PerCom2012]: Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context]]
 ----
-=== Algebraic Operational Transformation ===
+=== Achieving Probabilistic Atomicity with Well-Bounded Staleness and Low Read Latency in Distributed Datastores ===
-   Work in Progress.
+   Lingzhi Ouyang, Yu Huang, '''Hengfeng Wei''', Jian Lu
+  IEEE Trans. on Parallel and Distributed Systems, accepted, Nov. 2020.
-<div class="mw-collapsible">
+=== Jupiter Made Abstract, and Then Refined ===
-More details and comments are coming when the work is ready.
+  '''Hengfeng Wei''', Ruize Tang, Yu Huang, Jian Lu.
-</div>
+  “Jupiter Made Abstract, and then Refined”.
+  Journal of Computer Science and Technology, accepted, Aug. 2020.
+=== A Generic Specification Framework for Weakly Consistent Replicated Data Types ===
+  Xue Jiang, '''Hengfeng Wei''', Yu Huang.
+  “A Generic Specification Framework for Weakly Consistent Replicated Data Types”.
+  In Proceedings of the 39th International Symposium on Reliable Distributed Systems (SRDS 2020). Accepted. (To Appear).
+=== Fine-grained Analysis on Fast Implementations of Multi-writer Atomic Registers of Multi-writer Atomic Registers ===
+  Kaile Huang, Yu Huang, and '''Hengfeng Wei'''.
+  “Fine-grained Analysis on Fast Implementations of Multi-writer Atomic Registers of Multi-writer Atomic Registers”.
+  In Proceedings of the ACM Symposium on Principles of Distributed Computing (PODC 2020), 2020.
 ----
-=== CSS for Jupiter ===
+=== PaxosStore中共识算法TPaxos的推导、规约与精化 ===
+  易星辰, '''魏恒峰''', 黄宇, 乔磊, 吕建.
+  PaxosStore中共识算法TPaxos的推导、规约与精化.
+  软件学报 2020. 2020年第8期.
+----
+=== CRDT协议的TLA+ 描述与验证 ===
+  易星辰, '''魏恒峰''', 黄宇, 吕建.
+  CRDT协议的TLA+ 描述与验证.
+  软件学报 2020. 2020年第6期.
+----
+=== Specification and Implementation of Replicated List: The Jupiter Protocol Revisited ===
-   Work Under Review.
+   '''Hengfeng Wei''', Yu Huang, and Jian Lu.
+  “Specification and Implementation of Replicated List: The Jupiter Protocol Revisited”.
+  In: 22nd International Conference on Principles of Distributed Systems, OPODIS 2018, December 17-19, 2018, Hong Kong, China.
+, 12:1–12:16. url: https://doi.org/10.4230/LIPIcs.OPODIS.2018.12
-<div class="mw-collapsible">
+  '''Hengfeng Wei''', Yu Huang, and Jian Lu.
-This work is inspired by the work on [http://software.imdea.org/~gotsman/papers/editing-podc16.pdf "Specification and Complexity of Collaborative Text Editing"] published in PODC'2016 by Hagit Attiya et al.
+  “Brief Announcement: Specification and Implementation of Replicated List: The Jupiter Protocol Revisited”.
+  In: Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing. PODC ’18.
+  Egham, United Kingdom: ACM, 2018, pp. 81–83. url: http://doi.acm.org/10.1145/3212734.3212
-More details and comments are coming when the work is ready.
+ [[Media:jupiter-podc18-ba.pdf | Paper: Jupiter@PODC-BA'2018]] [[Media:Jupiter-opodis18.pdf | Paper: Jupiter@OPODIS'2018]] [[Media:1708.04754.pdf | [Paper: Jupiter@arXiv (full version)]]]
+<div class="mw-collapsible mw-collapsed">
+This work is inspired by the work on [http://software.imdea.org/~gotsman/papers/editing-podc16.pdf "Specification and Complexity of Collaborative Text Editing"] published in PODC'2016 by Hagit Attiya et al.
 </div>
@@ 第64行： / 第115行： @@
    '''Hengfeng Wei''', Yu Huang, Jian Lu.
    Parameterized and Runtime-tunable Snapshot Isolation in Distributed Transactional Key-value Stores.
-   In ''Proc. of the 36th International Symposium on Reliable Distributed Systems (SRDS)'', pp. 21--33, Hong Kong, Chain, Sep.2017.
+   In ''Proc. of the 36th International Symposium on Reliable Distributed Systems (SRDS)'', pp. 21--33, Hong Kong, China, Sep.2017.
-   [https://cs.nju.edu.cn/yuhuang/huangyufiles/papers/2017-SRDS.pdf [Paper:RVSI (not camera-ready)]]
+   [[Media:SRDS17_Parameterized_and_Runtime-tunable_Snapshot_Isolation_in_Distributed_Transactional_Key-value_Stores.pdf|[Paper:RVSI@SRDS17]]]
-<div class="mw-collapsible">
+<div class="mw-collapsible mw-collapsed">
 The formal specification of RVSI (Relaxed Version Snapshot Isolation) in this work is partly inspired by the work on [https://ai2-s2-pdfs.s3.amazonaws.com/0590/4e9741b2d3d9090807408ac9fb5da344c21e.pdf "Relaxed Currency Serializability for Middle-Tier Caching and Replication"] published in SIGMOD'2006 by Philip A.Bernstein ''et al''.
-It is the first time we use Aliyun in our experiments. This will be the normal case in the future.
-'''''Important Lessons Learnt:'''''
-* Solve the real problems in realistic ways!
-  One can always find made up examples of ..., but it is hard to convince that ....
-  This paper does not go beyond ....                          --- From Reviewers
-* System research greatly matters!
-  The following is all about the experimental section, which is probably the weakest part of the paper.
-                                                              --- From Reviewers
 </div>
 ----
@@ 第90行： / 第130行： @@
    [http://ieeexplore.ieee.org/document/7547362/ [abstract@IEEE]] [[Media:Probabilistically-Atomic 2-Atomicity Enabling Almost Strong Consistency in Distributed Storage Systems.pdf | [Paper: PA2AM@TC'2017]]] [https://arxiv.org/abs/1507.01663 [Paper: PA2AM@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.
@@ 第114行： / 第154行： @@
    SCI: DJ5HS
-<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".
@@ 第136行： / 第176行： @@
 == Projects ==
-* [[Projects:_Jupiter_Simulator | Jupiter Simulator]] <span style="color:#0000FF; background:#CCCCCC"> [In Plan] </span>
-* TLA+ Book Translation <span style="color:#FFFF00; background:#00C000"> [https://bitbucket.org/hengxin/hyperbook-tla-cn [Work in Progress@Bitbucket]] </span>
-** Please contact me if you are also interested in it.
-* LaTeX Editor: [http://vim-latex.sourceforge.net/ Vim-LaTeX] Improved
-** Project structure
-** Label autocompletion and renaming
-* TikZ Editor (I am '''very''' interested in this project.)
-** [http://detexify.kirelabs.org/ Detexify] for TikZ
-** (Better) Code recommendation
 == Links ==
-* [http://hengxin.github.io/ hengxin@github.io]: A blog hosted on GitHub.
+* [https://github.com/hengxin hengxin@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.
-* [https://www.sharelatex.com?r=108a8e2a&rm=d&rs=b Online LaTeX Editor ShareLaTeX]
-* [https://www.engineeringvillage.com/search/quick.url EI@Engineering Village], [http://apps.webofknowledge.com/UA_GeneralSearch_input.do?product=UA&search_mode=GeneralSearch&SID=4EoDOslD9qyFHCCqvUS&preferencesSaved= SCI@Web of Science]
+* [http://stackexchange.com/users/2055160 hengxin@StackExchange]