diff options
| author |  Unknown <afd@afd-THINK> | 2012-09-24 10:38:24 +0100 |
|---|---|---|
| committer | Unknown <afd@afd-THINK> | 2012-09-24 10:38:24 +0100 |
| commit | 87ac84943ce59bd98704bb0251770c48810e1767 (patch) | |
| tree | 802dc75e9a1361d2843f3ced1aee27b0f9ef35b0 /Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs | |
| parent | 7a895df23fe9260196be1c86bac11486a8d895b2 (diff) | |
Support for barrier invariants.
Diffstat (limited to 'Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs')
| -rw-r--r-- | Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs | 62 |
1 files changed, 62 insertions, 0 deletions
diff --git a/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs b/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs new file mode 100644 index 00000000..df84cae8 --- /dev/null +++ b/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs @@ -0,0 +1,62 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify {
+ class BinaryBarrierInvariantDescriptor : BarrierInvariantDescriptor {
+
+ private List<Tuple<Expr, Expr>> InstantiationExprPairs;
+
+ public BinaryBarrierInvariantDescriptor(Expr Predicate, Expr BarrierInvariant, KernelDualiser Dualiser) :
+ base(Predicate, BarrierInvariant, Dualiser) {
+ InstantiationExprPairs = new List<Tuple<Expr, Expr>>();
+ }
+
+ public void AddInstantiationExprPair(Expr first, Expr second) {
+ InstantiationExprPairs.Add(new Tuple<Expr, Expr>(first, second));
+ }
+
+ internal override AssertCmd GetAssertCmd(QKeyValue Attributes) {
+ var vd = new VariableDualiser(1, null, null);
+ return new AssertCmd(
+ Token.NoToken,
+ Expr.Imp(GPUVerifier.ThreadsInSameGroup(),
+ vd.VisitExpr(Expr.Imp(Predicate, BarrierInvariant))),
+ Dualiser.MakeThreadSpecificAttributes(Attributes, 1));
+ }
+
+ internal override List<AssumeCmd> GetInstantiationCmds() {
+ var result = new List<AssumeCmd>();
+ foreach (var Instantiation in InstantiationExprPairs) {
+ foreach (var Thread in new int[] { 1, 2 }) {
+
+ var vd = new VariableDualiser(Thread, null, null);
+
+ var ThreadInstantiationExpr = vd.VisitExpr(Instantiation.Item1);
+ var OtherThreadInstantiationExpr = vd.VisitExpr(Instantiation.Item2);
+
+ var ti = new ThreadPairInstantiator(Dualiser.verifier, ThreadInstantiationExpr, OtherThreadInstantiationExpr, Thread);
+
+ result.Add(new AssumeCmd(
+ Token.NoToken,
+ Expr.Imp(vd.VisitExpr(Predicate),
+ Expr.Imp(
+ Expr.And(
+ Expr.And(
+ Expr.And(NonNegative(ThreadInstantiationExpr),
+ NotTooLarge(ThreadInstantiationExpr)),
+ Expr.And(NonNegative(OtherThreadInstantiationExpr),
+ NotTooLarge(OtherThreadInstantiationExpr))
+ ),
+ Expr.Neq(ThreadInstantiationExpr, OtherThreadInstantiationExpr)),
+ ti.VisitExpr(BarrierInvariant)))));
+ }
+ }
+ return result;
+ }
+
+
+ }
+}
|