Skip to content

Commit

Permalink
Added ability to use variables as range parameters
Browse files Browse the repository at this point in the history
  • Loading branch information
Ellen Wittingen committed Dec 6, 2023
1 parent 9d3883a commit f28fed3
Show file tree
Hide file tree
Showing 8 changed files with 332 additions and 291 deletions.
1 change: 1 addition & 0 deletions examples/concepts/sycl/accessors/AllAccessModes.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ void test(int* a, int* b) {
context 1 < b_accessor.get_range().get(0);
context 2 < b_accessor.get_range().get(1);
context 1 < b_accessor.get_range().get(2);
context it.get_range(0) == 1;
context Perm(a_accessor[1][2], write);
context Perm(b_accessor[1][2][1], read);
*/
Expand Down
1 change: 1 addition & 0 deletions examples/concepts/sycl/addressSpaces/LocalAccessorUsage.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ void test() {

cgh.parallel_for(sycl::nd_range<1>(sycl::range<1>(20), sycl::range<1>(5)),
/*@
context it.get_local_id(0) < a_local_acc.get_range().get(0);
context Perm(a_local_acc[it.get_local_id(0)], write);
ensures a_local_acc[it.get_local_id(0)] == 10;
*/
Expand Down
12 changes: 12 additions & 0 deletions examples/concepts/sycl/buffers/AllBufferDimensions.cpp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
#include <sycl/sycl.hpp>

/*@
requires \pointer(a, 10, write);
requires \pointer(b, 10, write);
requires \pointer(c, 10, write);
*/
void test(bool* a, int* b, float* c) { // Does not work when using a[] instead of *a
sycl::buffer<bool, 1> aBuffer = sycl::buffer(a, sycl::range<1>(10));
sycl::buffer<int, 2> bBuffer = sycl::buffer(b, sycl::range<2>(2, 5));
sycl::buffer<float, 3> cBuffer = sycl::buffer(c, sycl::range<3>(2, 5, 1));
}
18 changes: 0 additions & 18 deletions examples/concepts/sycl/buffers/AllBufferTypes.cpp
View file

This file was deleted.

9 changes: 4 additions & 5 deletions examples/concepts/sycl/kernels/BasicKernel.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,15 @@ void test() {
[&](sycl::handler& cgh) {
cgh.parallel_for(sycl::range<3>(6,4,2),
/*@
requires it.get_id(0) > -1;
requires it.get_range(0) == 6;
ensures it.get_linear_id() > -1;
*/
[=] (sycl::item<3> it) {
int a = it.get_id(1);
//@ assert a < 6 && a >= 0;
//@ assert a < it.get_range(1) && a >= 0;
int b = it.get_linear_id();
//@ assert b < 48 && b >= 0;
int c = it.get_range(0);
//@ assert c == 6;
//@ assert b < it.get_range(0) * it.get_range(1) * it.get_range(2);
//@ assert b == it.get_id(2) + (it.get_id(1) * it.get_range(2)) + (it.get_id(0) * it.get_range(1) * it.get_range(2));
}
);
}
Expand Down
183 changes: 56 additions & 127 deletions res/universal/res/cpp/sycl/sycl.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,134 +22,71 @@ namespace sycl {
int get(int dimension);
}

// See SYCL spec 3.11.1 for the linearization formulas
//@ pure int linearize2(int id0, int id1, int r1) = id1 + (id0 * r1);
//@ pure int linearize3(int id0, int id1, int id2, int r1, int r2) = id2 + (id1 * r2) + (id0 * r1 * r2);
// See SYCL spec 3.11.1 for the linearization formulas
/*@
ghost
requires id0 >= 0 && id0 < r0 && id1 >= 0 && id1 < r1;
requires r0 >= 0 && r1 >= 0;
ensures \result == id1 + (id0 * r1);
ensures \result >= 0 && \result < r0 * r1;
pure int linearize2(int id0, int id1, int r0, int r1);
ghost
requires id0 >= 0 && id0 < r0 && id1 >= 0 && id1 < r1 && id2 >= 0 && id2 < r2;
requires r0 >= 0 && r1 >= 0 && r2 >= 0;
ensures \result == id2 + (id1 * r2) + (id0 * r1 * r2);
ensures \result >= 0 && \result < r0 * r1 * r2;
pure int linearize3(int id0, int id1, int id2, int r0, int r1, int r2);
ghost
requires |ids| == |ranges|;
requires (\forall int i; i >= 0 && i < |ids|; ids[i] >= 0 && ids[i] < ranges[i]);
ensures |ids| == 1 ==> \result == ids[0];
ensures |ids| == 2 ==> \result == sycl::linearize2(ids[0], ids[1], ranges[0], ranges[1]);
ensures |ids| == 3 ==> \result == sycl::linearize3(ids[0], ids[1], ids[2], ranges[0], ranges[1], ranges[2]);
pure int get_linear_id(seq<int> ids, seq<int> ranges);
*/

namespace item {
/*@
given seq<int> ids;
requires dimension >= 0;
requires dimension < |ids|;
ensures \result == ids[dimension];
@*/
/*@ pure @*/ int get_id(int dimension);

/*@
given seq<int> ranges;
requires dimension >= 0;
requires dimension < |ranges|;
ensures \result == ranges[dimension];
@*/
/*@ pure @*/ int get_range(int dimension);

/*@
given seq<int> ids;
given seq<int> ranges;
requires |ids| == |ranges|;
ensures |ids| == 1 ==> \result == ids[0];
ensures |ids| == 2 ==> \result == sycl::linearize2(
sycl::item::get_id(0) given{ids = ids},
sycl::item::get_id(1) given{ids = ids},
sycl::item::get_range(1) given{ranges = ranges});
ensures |ids| == 3 ==> \result == sycl::linearize3(
sycl::item::get_id(0) given{ids = ids},
sycl::item::get_id(1) given{ids = ids},
sycl::item::get_id(2) given{ids = ids},
sycl::item::get_range(1) given{ranges = ranges},
sycl::item::get_range(2) given{ranges = ranges});
@*/
/*@ pure @*/ int get_linear_id();
int get_id(int dimension);

int get_range(int dimension);

int get_linear_id();
}

namespace nd_item {

/*@
given seq<int> ids;
requires dimension >= 0;
requires dimension < |ids|;
ensures \result == ids[dimension];
@*/
/*@ pure @*/ int get_local_id(int dimension);
int get_local_id(int dimension);

/*@
given seq<int> ranges;
requires dimension >= 0;
requires dimension < |ranges|;
ensures \result == ranges[dimension];
@*/
/*@ pure @*/ int get_local_range(int dimension);

/*@
given seq<int> ids;
given seq<int> ranges;
requires |ids| == |ranges|;
ensures |ids| == 1 ==> \result == ids[0];
ensures |ids| == 2 ==> \result == sycl::linearize2(
sycl::nd_item::get_local_id(0) given{ids = ids},
sycl::nd_item::get_local_id(1) given{ids = ids},
sycl::nd_item::get_local_range(1) given{ranges = ranges});
ensures |ids| == 3 ==> \result == sycl::linearize3(
sycl::nd_item::get_local_id(0) given{ids = ids},
sycl::nd_item::get_local_id(1) given{ids = ids},
sycl::nd_item::get_local_id(2) given{ids = ids},
sycl::nd_item::get_local_range(1) given{ranges = ranges},
sycl::nd_item::get_local_range(2) given{ranges = ranges});
@*/
/*@ pure @*/ int get_local_linear_id();
int get_local_range(int dimension);

/*@
given seq<int> ids;
requires dimension >= 0;
requires dimension < |ids|;
ensures \result == ids[dimension];
@*/
/*@ pure @*/ int get_group_id(int dimension);
int get_local_linear_id();

/*@
given seq<int> ranges;
requires dimension >= 0;
requires dimension < |ranges|;
ensures \result == ranges[dimension];
@*/
/*@ pure @*/ int get_group_range(int dimension);
int get_group_id(int dimension);

/*@
given seq<int> ids;
given seq<int> ranges;
requires |ids| == |ranges|;
ensures |ids| == 1 ==> \result == ids[0];
ensures |ids| == 2 ==> \result == sycl::linearize2(
sycl::nd_item::get_group_id(0) given{ids = ids},
sycl::nd_item::get_group_id(1) given{ids = ids},
sycl::nd_item::get_group_range(1) given{ranges = ranges});
ensures |ids| == 3 ==> \result == sycl::linearize3(
sycl::nd_item::get_group_id(0) given{ids = ids},
sycl::nd_item::get_group_id(1) given{ids = ids},
sycl::nd_item::get_group_id(2) given{ids = ids},
sycl::nd_item::get_group_range(1) given{ranges = ranges},
sycl::nd_item::get_group_range(2) given{ranges = ranges});
@*/
/*@ pure @*/ int get_group_linear_id();
int get_group_range(int dimension);

int get_group_linear_id();

/*@
given seq<int> groupIds;
given seq<int> localIds;
given seq<int> groupRanges;
requires |groupIds| == |localIds| && |localIds| == |groupRanges|;
requires dimension >= 0;
requires dimension < |groupIds|;
given seq<int> localRanges;
requires |groupIds| == |localIds| && |localIds| == |groupRanges| && |groupRanges| == |localRanges|;
requires dimension >= 0 && dimension < |groupIds|;
requires groupRanges[dimension] > 0;
ensures \result == groupIds[dimension] + (localIds[dimension] * groupRanges[dimension]);
ensures \result >= 0 && \result < sycl::nd_item::get_global_range(dimension) given{groupRanges = groupRanges, localRanges = localRanges};
@*/
/*@ pure @*/ int get_global_id(int dimension);

/*@
given seq<int> groupRanges;
given seq<int> localRanges;
requires |groupRanges| == |localRanges|;
requires dimension >= 0;
requires dimension < |groupRanges|;
requires dimension >= 0 && dimension < |groupRanges|;
ensures \result == groupRanges[dimension] * localRanges[dimension];
@*/
/*@ pure @*/ int get_global_range(int dimension);
Expand All @@ -160,41 +97,33 @@ namespace sycl {
given seq<int> groupRanges;
given seq<int> localRanges;
requires |groupIds| == |localIds| && |localIds| == |groupRanges| && |groupRanges| == |localRanges|;
ensures |groupIds| == 1 ==> \result == sycl::nd_item::get_global_id(0) given {groupIds = groupIds, localIds = localIds, groupRanges = groupRanges};
requires (\forall int i; i >= 0 && i < |groupIds|;
sycl::nd_item::get_global_id(i) given{groupIds = groupIds, localIds = localIds, groupRanges = groupRanges, localRanges = localRanges} >= 0 &&
sycl::nd_item::get_global_id(i) given{groupIds = groupIds, localIds = localIds, groupRanges = groupRanges, localRanges = localRanges} < sycl::nd_item::get_global_range(i) given{groupRanges = groupRanges, localRanges = localRanges} &&
sycl::nd_item::get_global_range(i) given{groupRanges = groupRanges, localRanges = localRanges} >= 0);
ensures |groupIds| == 1 ==> \result == sycl::nd_item::get_global_id(0) given {groupIds = groupIds, localIds = localIds, groupRanges = groupRanges, localRanges = localRanges};
ensures |groupIds| == 2 ==> \result == sycl::linearize2(
sycl::nd_item::get_global_id(0) given{groupIds = groupIds, localIds = localIds, groupRanges = groupRanges},
sycl::nd_item::get_global_id(1) given{groupIds = groupIds, localIds = localIds, groupRanges = groupRanges},
sycl::nd_item::get_global_id(0) given{groupIds = groupIds, localIds = localIds, groupRanges = groupRanges, localRanges = localRanges},
sycl::nd_item::get_global_id(1) given{groupIds = groupIds, localIds = localIds, groupRanges = groupRanges, localRanges = localRanges},
sycl::nd_item::get_global_range(0) given{groupRanges = groupRanges, localRanges = localRanges},
sycl::nd_item::get_global_range(1) given{groupRanges = groupRanges, localRanges = localRanges});
ensures |groupIds| == 3 ==> \result == sycl::linearize3(
sycl::nd_item::get_global_id(0) given{groupIds = groupIds, localIds = localIds, groupRanges = groupRanges},
sycl::nd_item::get_global_id(1) given{groupIds = groupIds, localIds = localIds, groupRanges = groupRanges},
sycl::nd_item::get_global_id(2) given{groupIds = groupIds, localIds = localIds, groupRanges = groupRanges},
sycl::nd_item::get_global_id(0) given{groupIds = groupIds, localIds = localIds, groupRanges = groupRanges, localRanges = localRanges},
sycl::nd_item::get_global_id(1) given{groupIds = groupIds, localIds = localIds, groupRanges = groupRanges, localRanges = localRanges},
sycl::nd_item::get_global_id(2) given{groupIds = groupIds, localIds = localIds, groupRanges = groupRanges, localRanges = localRanges},
sycl::nd_item::get_global_range(0) given{groupRanges = groupRanges, localRanges = localRanges},
sycl::nd_item::get_global_range(1) given{groupRanges = groupRanges, localRanges = localRanges},
sycl::nd_item::get_global_range(2) given{groupRanges = groupRanges, localRanges = localRanges});
@*/
/*@ pure @*/ int get_global_linear_id();
}

namespace accessor {
/*@
ghost
requires id0 >= 0 && id0 < r0 && id1 >= 0 && id1 < r1;
requires r0 >= 0 && r1 >= 0;
ensures \result == id1 + (id0 * r1);
ensures \result >= 0 && \result < r0 * r1;
pure int linearize_2_indices(int id0, int id1, int r0, int r1);
ghost
requires id0 >= 0 && id0 < r0 && id1 >= 0 && id1 < r1 && id2 >= 0 && id2 < r2;
requires r0 >= 0 && r1 >= 0 && r2 >= 0;
ensures \result == id2 + (id1 * r2) + (id0 * r1 * r2);
ensures \result >= 0 && \result < r0 * r1 * r2;
pure int linearize_3_indices(int id0, int id1, int id2, int r0, int r1, int r2);
*/
sycl::range<1> get_range();
}

namespace local_accessor {
sycl::range<1> get_range();
sycl::range<2> get_range();
sycl::range<3> get_range();
}

}
Loading

0 comments on commit f28fed3

Please sign in to comment.