3

我看到类似在Linux RCU 测试和用于 CBMC 分析的 pthread 包装器__CPROVER_fence("RRfence", "RWfence");等项目中使用的代码。我查看了在线文档，但在发送到此 CBMC 函数的字符串中没有发现任何文本。

有哪些可用参数__CPROVER_fence？

我的看法是，它是一个注释/函数，用于表示由实际实现执行的障碍/栅栏。即，它是真实功能的分析存根。显然参数表示屏障的类型，但我没有找到实际参数和相应屏障类型的参考。即，“RRFence”是一个读栅栏，这意味着在此点之前的读取将在此点之后的读取之前完成（作为猜测）。

4

1 回答 1

2

使用源卢克。

所有符号都是“栅栏”，表示某些 CPU 屏障原语阻止了危险类型的发生。因此，所有先前的“读/写”都将在随后的“读/写”之前提交到缓存。“函数”可以接受这些值的任何组合/排列。

'cumul'版本记录在Herding cats...的第 4.4.2 节中，它们是“传递”围栏，表明所有线程/核心都将看到排序。

事实上，正如Hasturkun所指出的，有 8 个注释被CPROVER_fence(). 有关详细信息以及其他引用的论文，请参见维基百科危险。

  • RRFence，不是特定的危险，但可能导致事件级联
  • RWFence，这是一种反依赖，可能对依赖项有问题。
  • WRFence，仅涉及一个变量的特定危害
  • WWFence，只有一个“变量”可能导致输出危害。
  • WW累积
  • RR累积
  • RWcumul
  • WRcumul

'cumul' 版本类似于普通的 'fence' ，除了所有核心都保留了顺序。例如，在 ARM CPU 上，所有栅栏都是 'cumul' 类型。直接的“围栏”仅适用于无序问题，例如单个内核的管道和/或写入缓冲区。

所有符号都是“栅栏”，表示某些 CPU 屏障原语阻止了危险类型的发生。因此，所有先前的“读/写”都将在随后的“读/写”之前提交。“函数”可以接受这些值的任何排列。

一些不依赖于其他一致值的计数器之类的东西只需要一些栅栏就可以了。但是，其他值/元组/结构是多地址的（加载/存储非原子），并且可能需要以一致的方式读取/写入多个值。相互依赖访问的分类表 III。石蕊测试的词汇表放牧猫的名字......

CProver的“弱内存的软件验证”页面是该主题的罗塞塔石碑。它主要指的是“火枪手”工具，但进一步阅读会发现许多概念都包含在 CBMC 工具中。甚至页面的 URL 也包含“wmm”，它也在“goto-instrument”目录中作为“wmm”实现此功能。

  • 关于弱记忆的论文- 第 1 节结尾（第 A:5）详细介绍了将这些模型纳入 CBMC。模型是 TSO、PSO、RMO 和 Power。这些可以在“cbmc/src/goto-instrument/wmm/wmm.h”中找到。
  • 通过程序转换对弱内存进行软件验证描述了对 PostgreSQL 的修复和 Linux RCU 代码的检测；因此，引用的开源项目可能源自 CBMC 弱内存实现者，这可能是因为没有在线文档。

目录cbmc-concurrency和ansi-c有许多使用 theCPROVER_fence()和其他内存建模原语的示例。

pthread_mutex_lock()用于分析的示例 C 证明程序代码，

inline int pthread_mutex_lock(pthread_mutex_t *mutex)
{
  __CPROVER_HIDE:;
  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
  __CPROVER_assert(__CPROVER_get_must(mutex, "mutex-init"),
                   "mutex must be initialized");

  __CPROVER_assert(!__CPROVER_get_may(mutex, "mutex-destroyed"),
                   "mutex must not be destroyed");

  __CPROVER_assert(__CPROVER_get_must(mutex, "mutex-recursive") ||
                   !__CPROVER_get_may(mutex, "mutex-locked"),
                   "attempt to lock non-recurisive locked mutex");

  __CPROVER_set_must(mutex, "mutex-locked");
  __CPROVER_set_may(mutex, "mutex-locked");

  __CPROVER_assert(*((__CPROVER_mutex_t *)mutex)!=-1,
    "mutex not initialised or destroyed");
  #else
  __CPROVER_atomic_begin();
  __CPROVER_assume(!*((__CPROVER_mutex_t *)mutex));
  *((__CPROVER_mutex_t *)mutex)=1;
  __CPROVER_atomic_end();

  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence",
                  "WWcumul", "RRcumul", "RWcumul", "WRcumul");
  #endif

  return 0; // we never fail
}

我的理解是，它正在检查，

  • 只有一个锁
  • 锁在调用之前被初始化
  • 锁在持有时不会被破坏
  • 锁定时不会重新初始化
  • 调用后，所有弱排序内存项都被解析（所有缓存被刷新）。

有趣的是，man pthread_mutex_lock()没有说任何关于 CPU 同步或栅栏的内容。我们有互斥/锁编程的优先级反转、死锁等，但它也有管道性能的代价。实际上，在 ARM/Linux/glibc 上，调用kuser_cmpxchg32_fixupsmp_dmb arm即可满足此要求。类似的回归测试显示pthread_create()了写入缓冲区在初始线程启动时可能使值处于不确定状态的失败，除非插入屏障因为pthread_create()没有此同步。

看起来这项工作是相当新的（按照某些标准），2013 年的论文和 2016 年的 Linux RCU 提交。作者可能希望保持 API 流畅。可能他们更专注于证明证明者的更有趣的任务，并且没有时间记录这个接口。

注意：答案的早期版本假定此 API 涵盖了与非缓存总线主机的缓存同步。事实并非如此。如果担心的话，尝试使用的系统程序员cbmc需要使用其他机制。

于 2021-12-03T16:33:08.023 回答