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

来自Algorithm Wiki
跳转至： 导航、 搜索
（→‎Publications： +rvsi）
（→‎Publications： +RVSI@SRDS'2017）
第25行： 第25行：
 
== Publications ==
 
== Publications ==
  
−
* RVSI --- Under Review
+
* [[#JCSS | JCSS: CSS for Jupiter (WIP)]]
−
* [[#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]]
+
* [[#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]]
−
* [[#Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas | VPC --- Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas]]
+
* [[#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]]
−
* [[#Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context | CTL3 --- Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context]]
+
* [[#Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas | VPC: Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas]]
 +
* [[#Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context | CTL3: Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context]]
 +
 
 +
----
 +
 
 +
=== CSS for Jupiter ===
 +
 
 +
  Work In Progress.
 +
 
 +
<div class="mw-collapsible">
 +
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'2017 by Hagit Attiya ''et al''.
 +
 
 +
More details and comments are coming when the work is ready.
 +
</div>
 +
 
 +
----
 +
 
 +
=== 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 Conference on Reliable Distributed Systems (SRDS)'', Sep., 2017.
 +
  [https://cs.nju.edu.cn/yuhuang/huangyufiles/papers/2017-SRDS.pdf [Paper:RVSI (not camera-ready)]]
 +
 
 +
<div class="mw-collapsible">
 +
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.
 +
</div>
  
 
----
 
----
第39行： 第67行：
 
   [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)]]
 
   [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 mw-collapsed">
+
<div class="mw-collapsible">
 
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.
  
第52行： 第80行：
 
: In the single-write model, PA2AM implements a regular register.
 
: In the single-write model, PA2AM implements a regular register.
 
</div>
 
</div>
 +
 +
----
  
 
=== Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas ===
 
=== Verifying Pipelined-RAM Consistency over Read/Write Traces of Data Replicas ===
第61行： 第91行：
 
   SCI: DJ5HS
 
   SCI: DJ5HS
  
−
<div class="mw-collapsible mw-collapsed">
+
<div class="mw-collapsible">
 
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".  
  
 
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.
 
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.
+
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 [http://www.nearly42.org/ Marzio De Biasi], the second author of this paper.
 
The NP-completeness proof for VPC-SD (along with VPC-MD) is mainly credited to [http://www.nearly42.org/ Marzio De Biasi], the second author of this paper.
 
</div>
 
</div>
 +
 +
----
  
 
=== Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context ===
 
=== Formal Specification and Runtime Detection of Temporal Properties for Asynchronous Context ===

2017年6月28日 (三) 14:48的版本



Profile

Hengfeng Wei (魏恒峰) 

 Institute of Computer Software
 State Key Laboratory for Novel Software Technology
 Department of Computer Science and Technology
 Nanjing University
 Addr: 163 Xianlin Road, Nanjing 210046, P. R. China

 Office: 302

Email me: hfwei@nju.edu.cn

Researches

I am interested in Distributed Computing Theory and Formal Methods.

Publications

CSS for Jupiter

 Work In Progress.

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

More details and comments are coming when the work is ready.

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 Conference on Reliable Distributed Systems (SRDS), Sep., 2017.
 [Paper:RVSI (not camera-ready)]

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.

It is the first time we use Aliyun in our experiments. This will be the normal case in the future.

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

Links

取自“http://www.bigoh.net/wiki/index.php?title=用户:Hengfeng-Wei&oldid=939”