小编Jam*_*cox的帖子

以下GLSL计算着色器只是复制inImage到outImage.它源于更复杂的后处理过程.

在前几行中main(),单个线程将64个像素的数据加载到共享阵列中.然后,在同步之后,64个线程中的每一个将一个像素写入输出图像.

根据我的同步方式,我会得到不同的结果.我原本以为memoryBarrierShared()是正确的调用,但它会产生以下结果:

这与没有同步或使用相同的结果相同memoryBarrier().

如果我使用barrier(),我得到以下(所需)结果:

条带宽度为32像素,如果我将工作组大小更改为小于或等于32的任何值,我会得到正确的结果.

这里发生了什么？我误解了目的memoryBarrierShared()吗？为什么要barrier()工作？

#version 430

#define SIZE 64

layout (local_size_x = SIZE, local_size_y = 1, local_size_z = 1) in;

layout(rgba32f) uniform readonly  image2D inImage;
uniform writeonly image2D outImage;

shared vec4 shared_data[SIZE];

void main() {
    ivec2 base = ivec2(gl_WorkGroupID.xy * gl_WorkGroupSize.xy);
    ivec2 my_index = base + ivec2(gl_LocalInvocationID.x,0);

    if (gl_LocalInvocationID.x == 0) {
        for (int i = 0; i < SIZE; i++) …

在以下代码段中:

import qualified Data.Set as Set

data Nat = Zero | Succ Nat deriving (Eq, Show, Ord)

instance Enum Nat where
  pred (Succ x)     = x
  succ x            = Succ x
  toEnum 0          = Zero
  toEnum x          = Succ (toEnum (x-1))
  fromEnum Zero     = 0
  fromEnum (Succ x) = 1 + (fromEnum x)

nats :: [Nat]
nats = [Zero ..]

natSet :: Set.Set Nat
natSet = Set.fromList nats

为什么:

• elem (toEnum 100) nats == True

但

• Set.member (toEnum 100) natSet …

当在纸上推理时,我经常通过归纳使用一些列表的长度.我想在Coq中形式化这些参数,但似乎没有任何内置的方法来对列表的长度进行归纳.

我该如何进行这样的归纳？

更具体地说,我试图证明这个定理.在纸面上,我通过归纳证明了它的长度w.我的目标是在Coq中形式化这个证明.

我想为 Dafny 添加一些基本的便利功能，例如在 Dafny 中定义集合联合的能力（请参阅此问题）。但是 Dafny 的内部结构似乎没有很好的文档记录，我不知道从哪里开始。

如何添加这样的功能？