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

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.

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