5

JLS有两个结论：

  • C1：如果一个程序没有数据竞争，那么该程序的所有执行将看起来是顺序一致的：data-race-free => sequentially consistent
  • C2：如果一个程序正确同步，那么该程序的所有执行将看起来是顺序一致的：correctly synchronized => sequentially consistent

如果 C1 的反义词为真，那么我们可以得出结论：

  • C3：如果一个程序正确同步，那么它就没有数据竞争：correctly synchronized => data-race-free

但遗憾的是，JLS 中并没有这样的说法，所以我得出第四个结论：

  • C4：一个程序可以正确同步并且有数据竞争。

但我对这种方法并不满意，我想证明这个结论是正确的（或错误的），即使是以非正式的方式或样本方式。

首先，我认为显示包含数据竞争的多线程程序的顺序一致执行的代码段有助于理解和解决这个问题。

经过认真考虑，我仍然找不到合适的样品。那么请给我这样的代码段好吗？

4

3 回答 3

5

一个很好的例子可能是 String 的哈希码：

private int hash; // Default to 0

public int hashCode() {
    int h = hash;
    if (h == 0 && count > 0) {
        int off = offset;
        char val[] = value;
        int len = count;

        for (int i = 0; i < len; i++) {
            h = 31*h + val[off++];
        }
        hash = h;
    }
    return h;
}

这里存在数据竞争，因为哈希可以由不同的线程写入和读取，并且没有发生之前的关系（没有同步）。

但是程序是顺序一致的，因为线程不可能看到不是字符串的实际哈希码的哈希码（当线程执行哈希码方法时，它可以看到 0 并重新计算值，这是确定性的，或者它看到一个有效值）。这是有效的，因为 int 写入是原子的。

编辑

这个（几乎）相同的代码被破坏并且可能返回 0 的哈希码：

public int hashCode() {
    if (hash == 0 && count > 0) { //(1)
        int h = hash;
        int off = offset;
        char val[] = value;
        int len = count;

        for (int i = 0; i < len; i++) {
            h = 31*h + val[off++];
        }
        hash = h;
    }
    return hash; //(2)
}

因为 (1) 和 (2) 可以重新排序：(1) 可以读取非空值，而 (2) 将读取 0。这在第一个示例中不会发生，因为计算是在局部变量上进行的，并且返回value 也是那个局部变量，根据定义，它是线程安全的。

编辑 2

关于您的提议 C4，我认为这是不可能的：

当且仅当所有顺序一致的执行都没有数据竞争时，程序才能正确同步。

如果程序正确同步，则程序的所有执行都将显示为顺序一致（第 17.4.3 节）。

因此，如果程序正确同步：

  • 所有的执行看起来顺序一致。
  • 所有顺序一致的执行都没有数据竞争

因此我们可以得出结论，所有执行都没有数据竞争，因此程序没有数据竞争。

于 2012-08-17T15:00:43.507 回答
1

竞争条件意味着让程序的输出取决于谁首先到达特定点。例如，如果您有 2 个线程：T1 和 T2，如果您的程序输出为 X，如果 T1 首先到达程序中的点 P，并且如果程序的输出是 Y，如果 T2 先到达点 P，那么您就有竞争条件。

在伪代码中：

 Global variable i initialized to 6;
 Thread 1: 
       aquire(lock l)
             increment global variable i, i.e. i++;


 Thread 2: 
       aquire(lock l)
             double the value of global var i, i.e.: i*=2;

如果 T1 获得锁 l 第一和 T2 秒，则 i 的值将是 14 如果 T2 获得锁 l 第一和 T1 秒，则 i 的值将是 13

于 2012-08-17T13:31:02.020 回答
0

http://rsim.cs.illinois.edu/Pubs/popl05.pdf

证明似乎是这样的：

假设一个正确同步的程序的执行包含数据竞争，我们可以发现一个包含数据竞争的顺序执行，违反了“正确同步的程序”的定义[C1]

因此执行不能包含数据竞争。[C3] 从那里，可以证明执行是顺序一致的。[C2]

所以C3为真，用来证明C2。

于 2012-08-24T00:43:22.363 回答