Internals [https://www.youtube.com/watch?v=KN_i-ay0y1A&list=PLB1fSi1mbw6IKbZSPz9a2r2DbnHWnLbF-&index=32] Dispatch [https://llvm.org/docs/AMDGPUUsage.html#kernel-dispatch] HSA API [https://rocm.docs.amd.com/projects/ROCR-Runtime/en/docs-6.2.4/api-reference/api.html] HSA SPEC [https://hsafoundation.com/wp-content/uploads/2021/02/HSA-SysArch-1.2.pdf] CLC [https://github.com/HSAFoundation/CLOC]
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#![feature(ptr_metadata)] | |
// use libc; // 0.2.159 | |
use std::alloc::Layout; | |
use std::ptr::copy_nonoverlapping; | |
use std::mem::forget; | |
use std::ptr::metadata; | |
use std::ptr::DynMetadata; | |
fn main() { |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#![feature(debug_closure_helpers)] | |
use core::{alloc::Layout, mem::{align_of, size_of}}; | |
#[derive(Debug, Clone, Copy)] | |
struct MatrixDims { | |
rows: u8, | |
cols: u8 | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
def zmod : Nat -> Type | n => Quot (fun a b => a % n = b % n) | |
theorem prop_true_or_false : (p:Prop) -> p = False ∨ p = True := by | |
exact fun p => Or.symm (Classical.propComplete p) | |
theorem quot_ctor_inj : Quot.mk f a = Quot.mk f b -> a = b := by | |
intro k | |
-- injection k | |
admit |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
example {x:Rat} : 3 * x / 0.2 = (2 + 1/2) / (3 + 1/3) -> x = 1/20 := by | |
let is1 : (0.2:Rat) = 1/5 := by rfl | |
rw [is1] | |
let is2 : 3 * x / (1/5) = 3 * x * 5 := by | |
simp_all only [one_div, div_inv_eq_mul] | |
rw [is2] | |
let is3 : 3 * x * 5 = 15 * x := by | |
calc | |
3 * x * 5 = 3 * 5 * x := mul_right_comm 3 x 5 | |
3 * 5 * _ = 15 * x := by |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
def wmap : Type _ -> Type _ -> Type _ := | |
fun A B => @Subtype (Prod (A -> B) (B -> A)) fun ⟨ f , h ⟩ => ∀ i, h (f i) = i | |
def p1 : (w:wmap A B) -> let ⟨ ⟨ _ , h ⟩ , _ ⟩ := w; ∀ a:A , @Subtype B fun b => h b = a := by | |
intro w | |
let ⟨ ⟨ f , h ⟩ , p ⟩ := w | |
simp at p | |
simp | |
intro a |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# OPTIONS --type-in-type #-} | |
open import Agda.Builtin.Nat | |
open import Agda.Builtin.Bool | |
data Prod (L R : Set) : Set where | |
pair : L -> R -> Prod L R | |
data Unit : Set where | |
pt : Unit |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// for given number N, this function finds another number K such that | |
// (N * K) mod 2^64 = 1 | |
fn mult_mod_inv(n: u64) -> u64 { | |
assert!(n & 1 == 1, "Doesnt work for even numbers"); | |
assert!(n != 0, "Equation 0 mod N == 1 does not have a solution"); | |
let mut k = 1u64; | |
let mut i = 1u64; | |
for _ in 0 .. 64 { | |
i <<= 1; | |
let c = k.wrapping_mul(n); |
- Create this file
sudo touch /etc/apt/sources.list.d/rocm.list
- put this line in there
deb [arch=amd64] https://repo.radeon.com/rocm/apt/3.5.1/ xenial main
sudo apt update
- install ocl
sudo apt install rocm-opencl3.5.0
- this script doesnt write icd path to
/etc/OpenCL/vendors/
so that's on us touch /etc/OpenCL/vendors/amdocl64.icd
echo "/opt/rocm-3.5.1/opencl/lib/libamdocl64.so" > /etc/OpenCL/vendors/amdocl64.icd
- done. run
clinfo
. thing should work at this point
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// this kernel writes a value only if invoaction index is even *_* | |
// when _flag is true, the store adress gets computed to be beyound (1 << 48) byte location . | |
// apparently stores beyound valid adress space on gpu... just become noops! | |
#define store_if_true(Ty, addr, val, flag) \ | |
*((__global Ty*)(((unsigned long)addr) + (((unsigned long)(flag == 0)) * ((1LU << 48) - ((unsigned long)addr))))) = val; | |
__kernel void kern(__global unsigned int* buffer) { |
NewerOlder