Examples¶
This page shows what each project under examples/ does, what it prints, and which of its effect rows are worth reading. An effect row is the list of what a function may do, which the compiler infers and cairn doc prints. The test suite builds and runs every project where its tools are present.
Start with hello, the smallest complete project, and apps/kvstore, the shape of a real program. The demos each run with one make target.
| project | what it is |
|---|---|
| hello | the smallest project: a manifest, two source files, one task contract |
| systems | a decimal parser and a counting sort, with contracts for both |
| basics | three single files with no main, which the density check and the codegen benchmarks read |
| apps/kvstore | a key/value store on an append-only log that recovers from a torn write, with its index in memory |
| apps/service | a TCP key/value service on a line protocol |
| apps/wordfreq | a word counter, run from the command line over the files it is given |
| apps/classifier | a network trained on the gradients derive grad writes, then run quantized |
| apps/panel | an inventory screen drawn on the CPU, one task per frame |
| apps/analytics | a columnar engine whose table types are generated by recipes |
| apps/simulator | one Jacobi stencil run three ways, as a loop, on host threads and on the device, agreeing bit for bit |
| apps/gpu_pipeline | upload, map, compact, reduce, download, checked against the host |
| apps/matmul | an f16 layer multiplied by mma_unordered and held to its contract |
| interop | a C++ program calling a CAIRN library through its generated header |
| embedded | an AArch64 image with no operating system, run under QEMU, and a guard that fails |
| proof_scope | what cairn verify covers and what it cannot reach |
| sketch | one named choice settled by SMT, with no model |
| agent | the fixture behind the edit and repair loop |
| implementations | one prefix sum, three validated implementations, one searched over its parameter, and a scripted agent session |
| cooperative | three cooperative kernels on host threads, held to plain loops, with their device build, a searched block shape and pipeline depth, and five refused programs |
| reduction | an f32 sum in one launch: wide streaming loads, warp and block sums, a finish, and the same sum through an atomic add |
| tensor | a transpose through a shared tile laid out three ways, and two tensor-core multiplies written with fragments |
| foreign | a vendored C++ histogram and a vendored CUDA kernel, each an implementation of a CAIRN reference |
| harness | two benchmark problems as CAIRN kernels, with the mappings that package them as submissions |
| bazel | a Bazel workspace that builds, runs and tests CAIRN code with nothing fetched |
apps/simulator, apps/gpu_pipeline, the gpu.toml configurations and foreign/device need nvcc and a CUDA device, and the suite runs their device code only under make gpu. That target ran each of them once, in the 1.1.0 session on an RTX 5070 Ti (evidence/v1_1/gpu). harness needs nvcc to compile its kernels. bazel needs Bazel. embedded needs qemu-system-aarch64 on an AArch64 host. Everything else needs only a C++20 compiler.
examples/hello¶
cairn run examples/hello # prints nothing and exits 0
cairn test examples/hello # "status": "passed-finite-tests", "cases": 81
src/math.cairn holds average, the floor of the mean of two u64 values, computed without overflowing an intermediate sum. tests/average.json pins it at 81 boundary pairs, u64 maxima included. The guide walks through the same function in the project cairn new writes.
examples/systems¶
cairn run examples/systems # exits 0
cairn test examples/systems # decimal_kind: 8 cases, sorted_even: 7 cases, both passed
src/parse.cairn answers with a sum, Value(u64), Invalid(at), Overflow(at) or Empty, where at is the offset of the byte at fault. It returns no sentinel value, and it detects an overflow before the overflow happens. src/sort.cairn keeps its histogram in stack counts:usize[256], so nothing is allocated, and the rw output cannot alias the ro input.
examples/basics¶
The density harness (tools/checks/density.py) and the codegen benchmarks read these files.
cairn check examples/basics/native.cairn # "functions": 23
cairn check examples/basics/family.cairn # "functions": 256
cairn check examples/basics/wire.cairn # "functions": 3
native.cairn samples the breadth of the language: records, sums, each loops, compact, checked arithmetic, explicit conversions and every kind of guard. family.cairn is five lines, and its family gain = scale[1..257]; makes 256 typed specializations. wire.cairn is one record and one derive wire, whose output cairn expand prints.
examples/apps/kvstore¶
A key/value store that survives a crash: an append-only log of checksummed records, an index in memory, put, get and delete, reopening by replaying the log, and compaction. main runs the whole scenario against a file of its own and returns 0 only if every check passes.
cairn run examples/apps/kvstore
kvstore: self-check passed
derive wire for Header; writes the codec of the 16-byte header, little-endian. A linear File lives beside the store's state, outside it, and defer io.close(f) closes it on the failing path of every try too. Map[u64, Record] owns the key and value bytes: replacing a key releases the old value, and remove moves it out. A hit is checked byte for byte, so a digest collision is a miss.
replay stops at the first short, truncated or corrupt record and truncates the file there. The scenario tears the log twice and expects both tears to vanish. These are the effect rows, leaving out diverge, ffi:__errno_location, ffi_precondition, local_read, local_write and stack_storage:
put alloc, ffi:fsync, ffi:write, free, io, mmio, read:f, read:key, read:s, read:value,
trap, write:s, zero_init
replay alloc, ffi:ftruncate, ffi:lseek, ffi:read, free, io, mmio, read:f, read:s, trap,
write:s, zero_init
compact_log ffi:close, ffi:fsync, ffi:open, ffi:rename, ffi:write, io, mmio, read:path, read:s,
read:temp, trap, zero_init
put carries ffi:fsync, so durability shows in the row of everything that calls it. compact_log has no alloc, because it copies through one header on the stack and the existing storage.
examples/apps/service¶
A TCP key/value service on 127.0.0.1. It serves many clients at once from one thread, and a client shuts it down.
put <key> <value> -> +ok
get <key> -> = <value> | -missing
del <key> -> +ok | -missing
quit -> +bye, and the service exits 0
anything else -> -error
cairn run examples/apps/service # until a client says quit: "service: listening on 39800"
printf 'put a hello\nget a\ndel a\nget a\nquit\n' | nc 127.0.0.1 39800
+ok
= hello
+ok
-missing
+bye
One I/O ring holds the accept and every client's receive in flight, and q.next(tag, result) answers whichever finished first. A receive's buffer comes back with its result and goes into the next receive. The test holds three clients at once and checks that the process never has a second thread. On quit, run cancels the accept and every idle receive, and defer wait(q) collects them before the listener closes.
A function cannot return a borrow, so word_end returns an index and the caller takes the part, find(t, k, line[key_lo..key_hi]). Shifting a client's pending line down is an ordinary loop, because mem.copy would be refused there with E-ALIAS. The rows leave out the same effects as above:
respond alloc, ffi:send, free, io, mmio, read:line, read:t, trap, write:t, zero_init
take_in ... read:c, read:got, write:c, write:t
admit alloc, ffi:close, ffi:send, free, io, mmio, read:clients, read:q, write:clients, write:q, trap, zero_init
hang_up ffi:close, io, read:clients, trap, write:clients
run + ffi:socket, ffi:bind, ffi:listen, ffi:setsockopt, ffi:close, ffi:write
The only allocation per request is the answer to get, which respond builds in a Vec. A reply is a blocking send, so a client that stops reading its replies can still stall the service.
Overload gets an answer and never a trap. A 33rd client hears -busy and is closed. A failed accept, as when descriptors run out, is retried after a q.timeout of ten milliseconds, so the loop does not spin. Without io_uring, q.status() is negative, and the service prints service: no io_uring here, errno 24 and exits 2. tests/projects/test_apps.py provokes all three.
examples/apps/wordfreq¶
wordfreq prints the most frequent words of the files it is given, then the totals. A word is a run of ASCII letters and digits, folded to lowercase, and ties go in byte order. tale.txt is the opening of A Tale of Two Cities.
cairn run examples/apps/wordfreq -- -n 5 examples/apps/wordfreq/tale.txt
14 the
12 of
11 was
10 it
4 we
119 words, 58 distinct
It reads arguments and files through std.env and std.fs, keys a Map by a Word that implements Hash and Eq over its bytes, and aligns the table with std.fmt. counts.update(word, |c:rw<u64>| { c += 1; }) lends the closure the count alone, and a closure that reached for the map would be E-ALIAS. An unreadable file exits 1 with its errno, and bad arguments print the usage and exit 2. tests/projects/test_wordfreq.py compares every line with Python's Counter, under both compilers and under AddressSanitizer.
examples/apps/classifier¶
A network with eight tanh units learns which points of the square [-1.5, 1.5]^2 lie inside the unit circle. src/model.cairn writes the network and its mean log-loss, and four derive grad lines generate every gradient it needs. src/main.cairn trains on 400 points by plain gradient descent, then runs the trained network with its parameters quantized to i8 and to f8e4m3, one scale per tensor, on 400 points it never saw.
cairn run examples/apps/classifier
loss before 0.847914
loss after 0.069376
train accuracy 0.992500
test accuracy 0.992500
i8 accuracy 0.992500
i8 drift 0.192714
f8e4m3 accuracy 0.995000
f8e4m3 drift 0.961371
derive grad[w, c, v, b] for loss; differentiates with respect to the parameters and leaves the points as data. The sums are let mut loops, because a function that reaches libm cannot run inside a reduce. Drift is the largest change quantization makes to the output before the logistic function. tests/projects/test_app_classifier.py retrains 40 steps in Python with a backward pass derived by hand and requires every printed number to agree, under both compilers; it also runs the full 800 steps under the sanitizers.
examples/apps/panel¶
An inventory screen: a list of six items and the detail of the selected one. A script of keys drives it, one frame per key, and std.draw draws each frame on the CPU, with no window. cairn shot runs it and hands back each frame.
cairn shot examples/apps/panel --symbol panel.ui.update
shot: 7 frames
frame 0: …/shot-v4oktum8/frame-0.png 3 marked
frame 1: …/shot-v4oktum8/frame-1.png 3 marked 3.589 ms after the one before
…
panel.ui.update: read:ui, trap, write:ui
update declares effects(read:ui, write:ui, trap), so an allocation added to it is E-EFFECT-CEILING. Each frame is spawn render.frame(canvas, sheet, shown), which draws a copy of the state while main applies the next key. Touching the canvas before wait is E-LEASED, and a frame without its wait is E-LINEAR-LEAK.
The frame marks its panels in a Layout, which draw.capture writes beside the frame when CAIRN_SHOT names a directory. test layout holds the panels on screen and apart without reading a pixel. demos/visual is the same loop with an agent in it.
examples/apps/analytics¶
A million trades encoded with derive wire on disk, 21 bytes a row and 21 MB in all, are read back into a structure of arrays, then filtered, aggregated and grouped four ways. The program is 775 lines of CAIRN over ten modules. Recipes generate every table type: Trade_table, Trade_get, Trade_summarize, Trade_unrolled_price, the Ord that sorts a row and the Aggregator impls behind the query plan.
Five of the recipes are the program's own, four in src/cols.cairn and one in src/agg.cairn; one of them, device_columns, is used only by the device configuration. wire, eq and ord come from the packaged library.
Every query is answered twice, and main returns 0 only if the two answers agree: by rows against by columns, compact against the loop it stands for, a sequential pass against host lanes, one pass against four tasks, a bound against a table lookup, and, in the device configuration, host against device.
cairn run examples/apps/analytics --timeout 240
analytics: rows ingested 1000000
analytics: rows above limit 523214
analytics: price total 8389514683164
analytics: kept total 6482140393436
analytics: distinct venues 8
analytics: ingest 25132 us
analytics: row vs column 2704 us
analytics: statistics 4570 us
analytics: filter 1954 us
analytics: derived columns 5717 us
analytics: group by venue 2513 us
analytics: every cross-check passed on the host
The device configuration is a second manifest, gpu.toml, because one @device view sends the whole program through nvcc. A machine without CUDA must still build the host engine, which takes 1.2 s.
cairn run examples/apps/analytics/gpu.toml --timeout 300
analytics: rows on the GPU 1000000
analytics: rows above limit 523214
analytics: price total 8389514683164
analytics: host queries 2244 us
analytics: upload 69 us
analytics: device queries 975 us
analytics: download 1928 us
analytics: queued pipeline 1123 us
analytics: the device agrees with the host bit for bit
columns, a recipe over one record type, generates the table record: one Buf per field, with the row count as its declared extent, so a column goes to every query whole and pays no part guard. unrolled[K] also takes a number (derive cols.unrolled[4] for Trade;, derive cols.unrolled[8] for sensor.Reading;), and derive folded[add_wrap] for SumAgg; makes an aggregator in one line.
There are two totals because they are two claims. reduce + traps if the total does not fit. reduce add_wrap gives the same result under any association, and the device's tree reduction is compared against it.
Four tasks take disjoint row ranges and scratch blocks. Overlap two blocks by one element, and the second spawn is E-LEASED. The lanes of map_par call the caller's closure (lane:f), and a closure that assigned what it captured would be E-PARALLEL-CALL. run_static[A:Aggregator], run_dyn(a:rw<dyn Aggregator>, ...) and a Vec[Dyn[Aggregator]] plan built at run time give the same numbers.
The device pipeline queues spawn transfer and spawn parallel ... after while the host folds its own copy from the same pinned staging buffer under a shared read-only lease. report.line takes ro<u8>[LABEL], so a label one space short is E-TYPE-MISMATCH.
cols.chain (empty)
agg.counting (empty)
schema.Trade_key read:row, trap
schema.Trade_total_qty read:c, trap checked `reduce +`
schema.std.core.Ord....Trade.less read:a, read:b derived, not written
agg.Aggregator....SumAgg.absorb read:self, write:self derived from add_wrap
query.notional_loop read:price, read:qty, write:out, trap
query.notional_par ... par:host
query.map_par[u64, u64] ... indirect_call, lane:f, par:host
query.venue_sums_tasks ... spawn, join, alloc, free
agg.run_static[SumAgg] read:a, read:xs, write:a, trap
agg.run_dyn ... dispatch
device.queued_notional ... spawn, join, par:device, transfer:h2d, transfer:d2h
In the runs above, measured on 2026-09-19 on a GH200 with CUDA 12.8 and clang 15.0.7, ingest dominates, host lanes do not pay off over 10^6 cheap elements, and the download costs nearly twice what the device queries do. The device configuration also agreed with the host on the RTX 5070 Ti in the 1.1.0 session (evidence/v1_1/gpu).
Three things are still awkward. The fold a recipe runs takes only an operator or a bare function name. A view's extent cannot be inferred from a literal. A recipe cannot express arithmetic between two named fields, so notional_of is written by hand.
examples/apps/simulator¶
A two-dimensional Jacobi heat sweep over a 1024x1024 grid, 16 sweeps, run as an ordinary loop, as host lanes and as device lanes. The program compares all three element by element and fails if any bit differs.
cairn run examples/apps/simulator --timeout 240
simulator: 1024x1024 grid, 16 Jacobi sweeps
simulator: sequential 38291 us
simulator: threads 3628 us
simulator: device up 283130 us
simulator: device 448 us
simulator: all three back ends agree bit for bit
step_loop, step_threads and step_device have the same body, and the @device views of the third alone make its lanes a kernel. The bits agree because the arithmetic lives in one function compiled for both sides, with contraction and reassociation forbidden on both. Each round sweeps a -> b then b -> a, so no owner moves, and transfer is the only crossing between host and device.
blend (empty)
interior trap
step_loop ffi_precondition, read:src, trap, write:out
step_threads ffi_precondition, par:host, read:src, trap, write:out
step_device ffi_precondition, par:device, read:src, trap, write:out
main ... gpu_alloc, gpu_free, transfer:h2d, transfer:d2h, par:host, par:device
Measured on 2026-09-19 on a GH200 with 64 cores, CUDA 12.8 and clang 15.0.7, host threads beat the loop by about 10x and the device by about 85x, after 283 ms to create the CUDA context on the first device allocation.
examples/apps/gpu_pipeline¶
Four device stages over 2^22 values, each one statement, are checked against the same four stages run on the host, and io.monotonic_ns times every phase.
cairn run examples/apps/gpu_pipeline --timeout 240
gpu_pipeline: 4194304 values, kept 524288
gpu_pipeline: host pipeline 3485 us
gpu_pipeline: upload 125 us
gpu_pipeline: device map 305 us
gpu_pipeline: device compact 600 us
gpu_pipeline: device reduce 155 us
gpu_pipeline: download 1647 us
gpu_pipeline: device result matches the host
The same compact and reduce become CUB stream compaction and a tree reduction when their views are on the device, and plain loops when they are not. The sum uses add_wrap, because the order of a fold on the device is unspecified (reduce). The kept prefix is a part, dev_kept[0..dev_used], with one guard at run time.
map_device ffi_precondition, par:device, read:src, trap, write:out
keep_device ffi_precondition, gpu_alloc, gpu_free, par:device, read:src, trap, write:out
sum_device ffi_precondition, gpu_alloc, gpu_free, par:device, read:src, trap
main ... alloc, free, gpu_alloc, gpu_free, io, par:device, transfer:h2d, transfer:d2h
gpu_alloc in keep_device and sum_device is the execution context's arena growing for CUB's temporary storage. The run above was measured on 2026-09-19 on a GH200 with CUDA 12.8.
examples/apps/matmul¶
One dense layer, out = x * w, with x and w rounded once from f32 to f16 and out accumulated in f32 by mma_unordered, the tensor-core multiply. The host configuration multiplies with the written loop and checks every output against the multiply's contract: the exact f64 sum over the same f16 values, within (inner + 1) * 2^-22 * sum |x * w|. Its two test blocks check that the host result is the written loop's bit for bit, and that no products leave every output as it was.
cairn run examples/apps/matmul
host layer: 200 x 136 x 72, 0 outputs outside the contract
gpu.toml replaces the entry with src/device_main.cairn, which moves the matrices to the device, multiplies a 256 x 512 x 1024 layer on the tensor cores and holds it to the same bound. That shape is whole 64 x 64 tiles with k and n multiples of 8, so both stages in shared memory load through asynchronous copies of 16 bytes. It kept the bound on the RTX 5070 Ti in the 1.1.0 session (evidence/v1_1/gpu), and nothing has timed it. cairn predict prices it from the published tensor peak, as a roofline, at low confidence:
cairn predict examples/apps/matmul/gpu.toml --symbol device_layer --at rows=256,cols=512,inner=1024,on=131072,xn=262144,wn=524288
The prediction is 11.4 us, most of it an assumed launch of 8 us, and 0.27 of the roofline. All three come from the specification until make calibrate-device measures the device.
host_layer ffi_precondition, read:w, read:x, trap, write:out
device_layer ffi_precondition, par:device, read:w, read:x, trap, write:out
main ... gpu_alloc, gpu_free, par:device, transfer:h2d, transfer:d2h
examples/interop¶
A CAIRN library called from a C++ program that owns its data. src/stats.cairn summarizes a series in one pass, scales it in place, sums sliding windows and names its trend as a sum. host/main.cpp includes the header that cairn build --header wrote, and the C++ compiler alone builds it. Built and run, it prints:
cairn build examples/interop --header
count 6, min 4, max 42, total 108
windows of 3: 0 0 27 39 54 81
trend up by 38, spread 38
scaled by 3/2: 6 .. 63
ct_Summary and ct_Trend cross the boundary by value, laid out exactly as the header states and the library checks. A vector goes in as its data() and size(), and cf_window_sums refuses an output that overlaps its input by aborting at its entry. spread calls summarize inside CAIRN, where it reaches the body directly, without the entry's checks. tools.md has the rules.
examples/embedded¶
A sensor log arrives over a wire as decimal fields, each ended by a comma, some of them malformed, on a machine with no operating system, no C library and no allocator. The program reports each bad field with the offset of the byte at fault, summarises the good ones with checked arithmetic, sorts them through a fixed histogram, and prints all of it over a PL011 UART.
cairn run examples/embedded # builds the image and runs it under QEMU
cairn build examples/embedded # the ELF alone, plus the receipt beside it
cairn freestanding: qemu virt, pl011 uart
log 23,19,31,7,42,19,x9,,99999999999999999999,
bad digit at 17
empty field at 20
too large at 40
readings 6 total 141 max 42 mean 23
sorted 7 19 19 23 31 42
ok
The image exits with fn main()'s return value, 0 here, and size reports 5411 bytes of text, with no data and no bss.
The UART driver is mmio_read[u32] and mmio_write[u32] inside unsafe { }. Each field goes to the parser as text[start..i], a part of the one borrowed view, with no copy and one guard, and the histogram is a stack array. There is no Buf, parallel or extern anywhere, and the freestanding target refuses all three (the freestanding target).
trap/ reads one element past an array of four. With no MMU the read would return whatever follows the array, and the bounds check stops it.
cairn run examples/embedded/trap
trap demo: reading window[4] of 4
The program never prints unreachable, and QEMU exits 134, the status a hosted shell reports for std::abort.
examples/proof_scope¶
reference.cairn is the specification, candidate.cairn a different implementation of the same five functions, and mixed.cairn a case the value model of cairn verify cannot describe.
cairn verify examples/proof_scope/reference.cairn examples/proof_scope/candidate.cairn --all
# "status": "smt-module-equivalent", covered: average, extent, shifted, smaller, total
cairn verify examples/proof_scope/reference.cairn examples/proof_scope/mixed.cairn --all
# "status": "incomplete", missing: extent, shifted; extra: applied, moved; uncovered: applied, extent, moved, shifted
applied takes a callable, which the value model cannot express, so it is uncovered, and mixed.cairn stays incomplete even against itself. moved allocates a Buf and takes it, which the model does follow. native_proof and lean_proof are false in both answers. The answer is SMT equivalence of two sources under a restricted value model, and it proves nothing about machine code.
examples/sketch¶
The signature, the task and the reference belong to the host, and the search settles one named choice and nothing else. before.cairn returns (x + y) / 2, which overflows, and after.cairn is what the deterministic search picks.
python3 tools/ai/sketch_demo.py --out /tmp/sketchdemo
# {"status": "passed", "native_cases": 81, "model_used": false}
# searches: 4 candidates, 4 semantic checker calls, 8 SMT queries; then 3 calls and 6 queries from cache
average_0_reference-totality.smt2 and average_1_equivalence.smt2 are the two queries that settled it, in that order. choices.json holds the winning expression, and finite_task.json the 81 cases the result then runs against. The search tries a fixed list of four expressions, and it calls no model.
examples/agent¶
A task contract, a source with a deliberate error of one (>= where the task says strictly greater), the repaired source, and an adapter whose three answers are fixed in its code.
python3 tools/ai/demo.py --out /tmp/agentdemo
# {"status": "passed-reserved-finite-tests", "attempts": 3,
# "public_cases": 3, "reserved_cases": 5, "adapter_kind": "scripted-fixture"}
scripted_adapter.py stands in for a model and replies with a type error, then a behavioural error, then the correct body. task.json names the symbol, the allowed effects and the cases, some of them reserved, so the adapter never sees what it is finally judged on. prefix_sum.cairn is a second, unrelated symbol the harnesses use. demos/repair runs the same loop through the edit host on a larger program and ends with cairn diff.
examples/implementations¶
One reference, prefix, is the inclusive prefix sum written as the loop that defines it. It has three implementations:
prefix_by4takes four elements a step wheren % 4 == 0.prefix_by[K]takes one part ofKelements a step throughprefix_part[K], so a part's guard is checked once for itsKelements, withtune K in [4, 8, 16, 32].prefix_lanesis ascanon the lane pool oncen >= 65536, which the reference's effect ceiling (par:host) allows.
plan prefix use prefix_by4; selects the first, and main checks every length from 0 to 39 against n * (n + 1) / 2.
cairn run examples/implementations # prefix sums agree at every length from 0 to 39
cairn validate examples/implementations --symbol prefix_by4
# passed: prefix_by4 against prefix, 129 cases (46 ran it), finite-tested
# smt: smt-equivalent where ((((n % 4) == 0)) && (n >= 0 && n <= 4096)) && n <= 16
cairn validate examples/implementations --symbol "prefix_by[16]" # one instance at a time
cairn tune examples/implementations --symbol prefix --at n=1e6 # every instance, chosen only once validated
cairn test examples/implementations # replays regressions/prefix.json against every implementation
python3 examples/implementations/loop.py # the scripted session below, as JSON
bench/search/instances.py validates each instance, then lets cairn tune choose among them; evidence/v1_0/search records one run.
loop.py opens an implementation session on prefix under policy.json and replays four fixed replies. candidates/prefix_blocks_wrong.cairn restarts each block of eight at zero. Validation refuses it with the input it shrank to, n = 16 with a single 1 at xs[7], and keeps that input in regressions/prefix.json. The same reply with a looser tolerance is E-TOLERANCE, and with a smaller domain E-DOMAIN.
candidates/prefix_blocks.cairn carries the sum across blocks and validates. The replies are fixed text, and everything the host, the compiler and the native runs say is computed on each run.
examples/cooperative¶
Three cooperative regions, each a kernel whose threads share memory within a block. A transpose moves each 32 x 32 tile through a padded shared tile. Block sums halve 256 partial sums in shared memory and finish with a warp sum. Row sums read each row through a pipeline, at depth 2 and at depth 3. main runs them on host threads and holds each result to a plain loop.
cairn run examples/cooperative
transpose 96 x 64, 5 block sums and 3 row sums agree with plain loops
gpu.toml is the same kernels over @device views, with a driver that moves the data across. The suite compiles it for sm_120 and runs it only under make gpu, which ran it once, in the 1.1.0 session (evidence/v1_1/gpu). tuned.toml holds row_totals and an implementation, row_totals_tiled[T, D], whose block shape and pipeline depth cairn tune searches (tools.md). None of its instances is chosen until a validation on the device holds.
cairn tune examples/cooperative/tuned.toml --symbol row_totals --at rows=64,cols=1e5 --device-target sm_120
refused/ holds one program for each refusal of the phase and stage rules: conflicting_writes.cairn (E-COOP-CONFLICT), omitted_barrier.cairn (E-COOP-UNORDERED), premature_reuse.cairn (E-COOP-REUSE), stage_not_landed.cairn (E-STAGE-UNREADY) and stage_still_read.cairn (E-STAGE-BUSY). The host runs are clean under ThreadSanitizer with both compilers, and removing a barrier from the emitted C++ makes the sanitizer report a race (evidence/v1_0/cooperative).
examples/reduction¶
An f32 sum written the way a fast CUDA reduction is written, with nothing unsafe. Each thread streams its share of x, striding by the grid, sixteen bytes at a time with load_wide[4] and Cache.streaming. Each warp adds its threads' sums with reduce + warp, and each block adds its warps' sums through a shared array nobody zeroes. The region's finish adds the blocks' sums once every block is done.
The program fixes the order of every addition, so the sum is the same on every run with the same grid. sum_unordered is the same sum with no partials: each block adds its total into out[0] with atomic_add_unordered, in the order the blocks finish. main runs both on host threads and holds them to a plain loop: exactly on whole numbers whose every partial sum f32 holds, and within the bound of an f32 sum in any order on fractions.
cairn run examples/reduction
the one-pass and the atomic sums agree with a plain loop on host threads
gpu.toml is the same kernels over @device views, with a driver that moves the data across. The suite runs it emulated on host threads and compiles it for sm_120, where the sum's loop is one LDG.E.EF.128 a step with nothing in local memory (evidence/v1_1/kernels). The suite runs it on a GPU only under make gpu, which ran it once, in the 1.1.0 session on an RTX 5070 Ti. In the same session bench/device timed sum through its cq_sum entry at 330.7 us, against 329.1 us for a CUDA kernel written by hand that makes one pass, the medians of 60 calls at 2^26 f32 (evidence/v1_1/gpu).
examples/tensor¶
Three single files, each a program of cooperative regions with layouts. A layout states where each element of a tile is stored. transpose.cairn transposes through a 32 x 32 shared tile stored row-major, padded and swizzled. The threads are the same each time, and only the layout differs. cairn explain says what that changes: reading the tile a column at a time takes 32 bank ways row-major, and 1 padded or swizzled.
cairn run examples/tensor/transpose.cairn # exits 0 when all three transposes agree
cairn explain examples/tensor/transpose.cairn # bank_ways and conversions for each spread
tile64.cairn and tile32.cairn add a * b into c with tensor-core fragments, under the signature and contract of mma_unordered. numerics.md gives their two tilings and what their runs on the host showed. Both compile for sm_120, and on an RTX 5070 Ti each kept the contract on the suite's shapes (evidence/v1_0/tensor, evidence/v1_1/gpu).
examples/foreign¶
Two projects that bring existing code in as foreign implementations: vendored C++ or CUDA that stands in for a CAIRN reference and is tested against it. In foreign/host, vendor/histogram.cpp computes the histogram of 256 bins that histogram_u32 defines, and plan histogram_u32 use histogram_interleaved; runs it. In foreign/device, vendor/stencil.cu is a CUDA kernel for the blend of three points that stencil_1d defines, launched through launch(threads, block). vendor/parallel_gpu.cu is compiled and inspected with the program's flags, and not linked.
cairn run examples/foreign/host # bin 7 holds 7 samples
cairn foreign examples/foreign/host --implementation histogram_interleaved
cairn foreign examples/foreign/device --implementation stencil_tiled --device-target sm_120
tools.md shows what cairn foreign reports for each. The device kernel is compiled for sm_120 and inspected. Its validation against the reference runs only under make gpu, which ran it once, in the 1.1.0 session on an RTX 5070 Ti (evidence/v1_1/gpu).
examples/harness¶
Two benchmark problems written as CAIRN device kernels: GPU MODE's vectoradd_v2, which adds two float16 matrices, and KernelBench's level-1 ReLU. harness.toml maps GPU MODE's input tuple (A, B, output) onto vectoradd, and kernelbench.toml maps forward(x) onto relu, whose output the adapter allocates.
cairn export examples/harness --harness gpumode --symbol vectoradd --out out/vectoradd
cairn export examples/harness --harness kernelbench --symbol relu --mapping examples/harness/kernelbench.toml --out out/relu
Each command writes the submission, the export it embeds and a cairn.harness/1 record, and prints the commands that would evaluate or submit it (devices.md). It runs and submits nothing. Both kernels compile for sm_100a, and neither has run on a GPU.
examples/bazel¶
A Bazel workspace for rules_cairn, the Bazel rules for CAIRN code. tools.md says how the rules check and build it. The workspace holds two libraries, geometry and pricing, a binary shop and a test, each a .cairn file, and it fetches nothing.
cd examples/bazel && bazel test //...