|
| 1 | +// Vector addition kernel demonstrating Descend's safe GPU programming model |
| 2 | +// This function showcases extended borrow checking, memory safety, and execution context tracking |
| 3 | + |
| 4 | +// Generic function with type parameters: |
| 5 | +// - n: nat - Natural number parameter (for array size, though not used in this specific function) |
| 6 | +// - r: prv - Provenance parameter tracking memory region/lifetime for all references |
| 7 | +fn add<n: nat, r: prv>( |
| 8 | + // Shared reference to first input vector - multiple threads can read simultaneously |
| 9 | + // Memory space: gpu.global (GPU global memory) |
| 10 | + // Ownership: shrd (shared) - prevents write-after-read data races |
| 11 | + // Type: 16-element array of 16-bit signed integers |
| 12 | + a: &r shrd gpu.global [i16; 16], |
| 13 | + |
| 14 | + // Shared reference to second input vector - multiple threads can read simultaneously |
| 15 | + // Same memory space and ownership constraints as 'a' |
| 16 | + b: &r shrd gpu.global [i16; 16], |
| 17 | + |
| 18 | + // ERROR: This parameter should be declared as 'unq' (unique) instead of 'shrd' (shared) |
| 19 | + // because it's used for assignment (c = a + b). Shared references are read-only and |
| 20 | + // prevent data races by allowing multiple concurrent readers. Unique references are |
| 21 | + // required for write operations to ensure exclusive access and prevent race conditions. |
| 22 | + // The Descend compiler will detect this ownership violation and fail compilation. |
| 23 | + c: &r shrd gpu.global [i16; 16] |
| 24 | + |
| 25 | +// Execution context specification - defines how this function runs on GPU hardware |
| 26 | +// - grid: gpu.grid<X<1>, X<16>> - GPU execution grid with 1 block containing 16 threads |
| 27 | +// - The type system ensures GPU memory is only accessed in GPU execution contexts |
| 28 | +// - Prevents invalid cross-device memory accesses (CPU accessing GPU memory) |
| 29 | +) -[grid: gpu.grid<X<1>, X<16>>]-> () { |
| 30 | + |
| 31 | + // Vector addition operation - element-wise addition of arrays |
| 32 | + // The compiler generates safe parallel code that: |
| 33 | + // 1. Loads data from global memory to local memory for each thread |
| 34 | + // 2. Performs vectorized addition using HIVM dialect operations |
| 35 | + // 3. Stores results back to global memory safely |
| 36 | + // The ownership system ensures this operation is race-free |
| 37 | + // |
| 38 | + // LAZY LOADING: Descend's compiler implements lazy loading strategies: |
| 39 | + // - Memory loads are deferred until actually needed by computation |
| 40 | + // - The HIVM dialect generates 'hivm.hir.load' operations that load from |
| 41 | + // global memory (gm) to local memory (ub) only when data is accessed |
| 42 | + // - This minimizes memory bandwidth usage and improves cache efficiency |
| 43 | + // - The type system ensures loads happen in the correct execution context |
| 44 | + // - Shared references enable read-only access without unnecessary copies |
| 45 | + c = a + b; |
| 46 | + |
| 47 | + // Unit return value - indicates successful completion |
| 48 | + // In MLIR, this becomes a 'return' operation |
| 49 | + () |
| 50 | +} |
0 commit comments