A kernel as standalone MISRA C#
One task: take a kernel you already run on the CPU and emit it as a standalone C99 source pair for an embedded build, then show that the C computes the same bits as hawk’s own host build. The output includes no hawk, aether or eagle header, so it compiles on its own.
Time: ~5 min · Runs on: CPU · You need: hawk, NumPy and a C
compiler (cc, clang or gcc); with cppcheck installed the MISRA C:2012 check
runs too; reference: The embedded C target
Colab or Kaggle: run this first cell (it installs the packages and downloads the helper files this notebook uses). Elsewhere it only checks the imports.
The kernel#
Quadratic drag on a three-component state, the same kernel the reference page uses. Nothing in it knows about C:
import hawk
from hawk import Mutable, Param, Vector
from hawk.math import norm
@hawk.kernel
def drag(state: Vector[3], rho: Param, out: Mutable[Vector[3]]):
out = -rho * state * norm(state)
drag
<Kernel drag slots=3>
Export it#
hawk.embedded.export runs the whole pipeline: it checks the kernel’s IR
for anything the C target cannot build, renders the C, audits the text,
and compiles it under strict -std=c99 and -std=c11 warnings-as-errors.
When cppcheck is on the PATH it also runs the MISRA addon. It writes
three files:
import pathlib
import tempfile
import hawk.embedded
work = pathlib.Path(tempfile.mkdtemp())
art = hawk.embedded.export(drag, work / "c")
sorted(p.name for p in (work / "c").iterdir())
['drag.c', 'drag.embedded.json', 'drag.h']
The header is the whole contract for whoever calls the unit. It records
where the code came from (hawk version and digests of the walk and of the
kernel’s source), the worst-case budgets, and one row per argument: role,
direction, element type, shape and whether the caller must initialise it.
Planes are structure-of-arrays with a pitch of n_samples:
print(art.h_path.read_text())
/* drag.h -- generated by hawk 0.7.0; do not edit.
* TRACEABILITY:
* kernel drag
* hawk version 0.7.0
* walk digest bcc450195db6caa95fb54687b8b395c13f1bcffbf63d1c0ef69191cda2624a84
* kernel sha256 9361b9391b4dc2bbfbece7e388f9463910515d535cc0cf6298af0e7fd6749506
* scalar mode float64
* target c, MISRA C:2012+AMD, C99 dialect, serial
* profile EmbeddedProfile(max_trips=None, max_ops=None, max_stack_bytes=None, fp_domain='record', index_policy='clamp', require_cppcheck=False, c_std='c99')
* aether core aether-c/1
* BUDGETS (per sample, worst case):
* loop trips 0
* ops arith32 0, arith64 14, special32 0, special64 0, loads 3, gathers 0, chain32 0, chain64 3, chainSpecial32 0, chainSpecial64 0, stores 3
* fp64 ops 14
* static bytes tapes 0, carries 0, temporaries 72, total 72
* libm sqrt
* INTERFACE CONTRACT: planes are SoA; rank-1 extent N stores component c of sample i at
* base[(c * n_samples) + i]; rank-2 (R,C) at base[(((r*C)+c) * n_samples) + i]; rank-0 at
* base[i]. The pitch is ALWAYS n_samples, also for a partition [base, base+count).
* A runtime-length plane carries its length in the int64_t field after its pointer.
* field role dir dtype shape init-by-caller
* mut_out mutable out f64 (3,) no
* vin_state vec_in in f64 (3,) yes
* uni_rho uniform in f64 () yes (by value)
* drag_c() validates args and every pointer, 0 <= base <= n_samples and
* 0 <= count <= n_samples - base, returning HAWK_E_NULL / HAWK_E_RANGE untouched otherwise.
* Re-entrant, allocation-free. */
#ifndef HAWK_DRAG_H
#define HAWK_DRAG_H
#include <stdint.h>
#include <stddef.h>
#ifndef HAWK_EMBEDDED_TYPES
#define HAWK_EMBEDDED_TYPES 64
typedef double hawk_real_t;
typedef int64_t hawk_int_t;
typedef enum { HAWK_OK = 0, HAWK_E_NULL = 1, HAWK_E_RANGE = 2 } hawk_status_t;
#elif HAWK_EMBEDDED_TYPES != 64
#error "drag.h: float64 unit; another hawk header in this build defined hawk_real_t at a different width"
#endif
typedef struct {
hawk_real_t* mut_out; /* mutable out Vector[3] SoA, pitch n_samples */
const hawk_real_t* vin_state; /* vec_in in Vector[3] SoA, pitch n_samples */
hawk_real_t uni_rho; /* uniform in Scalar by value */
} drag_args_t;
hawk_status_t drag_c(const drag_args_t* args, int64_t base, int64_t count, int64_t n_samples);
#endif
The .c holds the computation. Everything it calls is inlined into the
file: aether’s reference C for each vector operation (aether_c_*), and
hawk’s own load and store helpers (hawk_*). Here is the per-sample loop
and the entry that validates its arguments before touching any plane:
print(art.c_path.read_text())
/* drag.c -- generated by hawk 0.7.0; do not edit. See drag.h. */
#include "drag.h"
#include <math.h>
#include <stdbool.h>
#if defined(__STDC_VERSION__) && (__STDC_VERSION__ >= 201112L)
_Static_assert(sizeof(hawk_real_t) == 8U, "drag.c: hawk_real_t is not the float64 width");
_Static_assert(sizeof(hawk_int_t) == 8U, "drag.c: hawk_int_t is not 64-bit");
#endif
#ifndef AETHER_C_F64_T
#define AETHER_C_F64_T
typedef double aether_c_f64_t;
#endif
#ifndef AETHER_C_F64_VEC3_T
#define AETHER_C_F64_VEC3_T
typedef struct { aether_c_f64_t v[3]; } aether_c_f64_vec3_t;
#endif
/* aether-c: vec_norm (3,) f64 aether-c/1 */
static inline aether_c_f64_t aether_c_f64_vec3_norm(aether_c_f64_vec3_t a)
{
return sqrt(((a.v[2] * a.v[2]) + ((a.v[1] * a.v[1]) + (a.v[0] * a.v[0]))));
}
/* aether-c: vec_scale (3,) f64 aether-c/1 */
static inline aether_c_f64_vec3_t aether_c_f64_vec3_scale(aether_c_f64_vec3_t a, aether_c_f64_t s)
{
aether_c_f64_vec3_t out;
out.v[0] = (s * a.v[0]);
out.v[1] = (s * a.v[1]);
out.v[2] = (s * a.v[2]);
return out;
}
/* hawk: load (3,) float64 */
static inline aether_c_f64_vec3_t hawk_vec3_load(const hawk_real_t* plane, int64_t i, int64_t pitch)
{
aether_c_f64_vec3_t out;
out.v[0] = plane[i];
out.v[1] = plane[pitch + i];
out.v[2] = plane[(2 * pitch) + i];
return out;
}
/* hawk: store (3,) float64 */
static inline void hawk_vec3_store(hawk_real_t* plane, int64_t i, int64_t pitch, aether_c_f64_vec3_t x)
{
plane[i] = x.v[0];
plane[pitch + i] = x.v[1];
plane[(2 * pitch) + i] = x.v[2];
}
static void drag_run(const drag_args_t* args, int64_t base, int64_t count, int64_t n_samples)
{
hawk_real_t* const mut_out = args->mut_out;
const hawk_real_t* const vin_state = args->vin_state;
const hawk_real_t uni_rho = args->uni_rho;
const int64_t hawk_end = base + count;
for (int64_t hawk_i = base; hawk_i < hawk_end; ++hawk_i) {
const aether_c_f64_vec3_t vin_state_i = hawk_vec3_load(vin_state, hawk_i, n_samples);
const aether_c_f64_vec3_t t3 = aether_c_f64_vec3_scale(vin_state_i, (-uni_rho));
const aether_c_f64_vec3_t t5 = aether_c_f64_vec3_scale(t3, aether_c_f64_vec3_norm(vin_state_i));
hawk_vec3_store(mut_out, hawk_i, n_samples, t5);
}
}
hawk_status_t drag_c(const drag_args_t* args, int64_t base, int64_t count, int64_t n_samples)
{
hawk_status_t status;
if (args == NULL) {
status = HAWK_E_NULL;
} else if ((args->mut_out == NULL) || (args->vin_state == NULL)) {
status = HAWK_E_NULL;
} else if ((base < INT64_C(0)) ||
(base > n_samples) ||
(count < INT64_C(0)) ||
(count > (n_samples - base))) {
status = HAWK_E_RANGE;
} else {
drag_run(args, base, count, n_samples);
status = HAWK_OK;
}
return status;
}
The report#
drag.embedded.json carries what the header summarises, in a form a
safety review or a CI gate can read. The budgets are per sample:
report = art.report
budgets = report["budgets"]
print("loop trips :", budgets["max_trips"])
print("fp64 ops :", budgets["fp64_ops"])
print("stack bytes :", budgets["static_bytes"]["total"])
print("libm :", report["libm"])
print("aether core :", report["core"], report["core_version"])
print("hawk helpers:", report["helpers"])
loop trips : 0
fp64 ops : 14
stack bytes : 72
libm : ['sqrt']
aether core : ['aether_c_f64_vec3_norm', 'aether_c_f64_vec3_scale'] aether-c/1
hawk helpers: ['hawk_vec3_load', 'hawk_vec3_store']
The interface rows are the machine-readable form of the header’s contract table:
for row in report["interface"]:
print(f'{row["field"]:10} {row["role"]:8} {row["direction"]:6} '
f'{row["dtype"]:8} {str(row["shape"]):6} init by caller: {row["init_by_caller"]}')
mut_out mutable out f64 [3] init by caller: False
vin_state vec_in in f64 [3] init by caller: True
uni_rho uniform in f64 [] init by caller: True
And the checks block records exactly what ran. A missing cppcheck
shows up as skipped, never as a silent pass; pass
EmbeddedProfile(require_cppcheck=True) to make it a refusal instead.
Every suppressed rule is a documented deviation with its reason in
report["deviations"]:
checks = report["checks"]
for cc in checks["cc"]:
print(f'cc -std={cc["std"]:4} rc={cc["rc"]}')
cppcheck = checks["cppcheck"]
if "skipped" in cppcheck:
print("cppcheck :", cppcheck["skipped"])
else:
print("cppcheck : rc", cppcheck["rc"], "findings", cppcheck["findings"])
print("deviations :", [d["rule"] for d in report["deviations"]])
cc -std=c99 rc=0
cc -std=c11 rc=0
cppcheck : rc 0 findings []
deviations : ['misra-c2012-8.7', 'misra-c2012-9.3', 'misra-c2012-2.3']
The same bits as the host build#
The C target is serial and bit-identical to hawk’s host C++ build under
the native profile, so the host build is the reference. Build it, run it,
then compile the C into a shared library and call it through ctypes.
Both sides keep floating-point contraction off: the C is compiled with
-ffp-contract=off, as any embedded build of this unit must be. The
comparison is on raw bytes, so a difference in the last bit, a -0.0
or a NaN payload would all count.
The ctypes structure below mirrors drag_args_t from the header, field
for field:
import ctypes
import hawk.artifact
import numpy as np
from hawk.embedded import toolchain
C_REAL = {"float64": ctypes.c_double, "float32": ctypes.c_float}
def c_drag(mode):
"""Export drag at ``mode``, compile it, and return a callable entry."""
unit = hawk.embedded.export(drag, work / f"c_{mode}", mode=mode)
lib = ctypes.CDLL(str(toolchain.compile_shared(unit.c_path,
work / f"libdrag_{mode}.so")))
real = C_REAL[mode]
class DragArgs(ctypes.Structure): # drag_args_t
_fields_ = [("mut_out", ctypes.POINTER(real)),
("vin_state", ctypes.POINTER(real)),
("uni_rho", real)]
lib.drag_c.argtypes = [ctypes.POINTER(DragArgs),
ctypes.c_int64, ctypes.c_int64, ctypes.c_int64]
lib.drag_c.restype = ctypes.c_int # hawk_status_t
def call(state, rho, out, base=0, count=None):
n = state.shape[1]
ptr = ctypes.POINTER(real)
args = DragArgs(None if out is None else out.ctypes.data_as(ptr),
state.ctypes.data_as(ptr), rho)
return lib.drag_c(ctypes.byref(args), base,
n - base if count is None else count, n)
return call
rng = np.random.default_rng(7)
n = 10_000
state64 = rng.normal(size=(3, n)) * 10.0 ** rng.integers(-3, 4, size=n)
rho = 1.225
for mode, dtype in (("float64", np.float64), ("float32", np.float32)):
state = np.ascontiguousarray(state64.astype(dtype))
rho_m = float(dtype(rho))
hawk.artifact.build(drag, work / f"host_{mode}", targets=("host",),
mode=mode, host_profile="native")
out_host = np.zeros((3, n), dtype)
hawk.run(hawk.load(work / f"host_{mode}", "drag"),
state=state, rho=rho_m, out=out_host)
out_c = np.zeros((3, n), dtype)
status = c_drag(mode)(state, rho_m, out_c)
same = out_c.tobytes() == out_host.tobytes()
print(f"{mode}: status {status}, {out_c.size} values, bit-identical: {same}")
float64: status 0, 30000 values, bit-identical: True
float32: status 0, 30000 values, bit-identical: True
The float32 unit is float end to end: typedef float hawk_real_t, sqrtf
and no double anywhere, so nothing is silently promoted:
f32 = (work / "c_float32" / "drag.c").read_text()
print("sqrtf calls:", f32.count("sqrtf("), "| 'double' tokens:", f32.count("double"))
sqrtf calls: 1 | 'double' tokens: 0
The entry checks its arguments#
drag_c takes a partition [base, base + count) of the batch and returns
a status instead of trusting its inputs. A partition writes its own
samples only, and the pitch stays n_samples:
call = c_drag("float64")
small = np.ascontiguousarray(state64[:, :8])
part = np.zeros((3, 8))
print("status:", call(small, rho, part, base=2, count=3))
print("samples written:", np.flatnonzero(part.any(axis=0)))
status: 0
samples written: [2 3 4]
A range outside the batch, or a null plane, is refused before any plane
is touched (HAWK_E_RANGE is 2, HAWK_E_NULL is 1):
untouched = np.zeros((3, 8))
print("base past the end:", call(small, rho, untouched, base=6, count=5))
print("null output plane:", call(small, rho, None))
print("output untouched :", not untouched.any())
base past the end: 2
null output plane: 1
output untouched : True
What the verify pass refuses#
Before any C is rendered, a verify pass walks the kernel’s IR. By default
anything it cannot guarantee is refused with an error that names the
kernel, the node and the rule, and nothing is written. An
EmbeddedProfile adds caps and tightens policies.
Index safety. A table read uses a runtime index, which the IR cannot prove in range. The C clamps it to the table’s length, a no-op on every call the host build defines, and the report lists the site:
from hawk import Index, Scalar, Table
from hawk.embedded import EmbeddedProfile
from hawk.ir import HawkError
@hawk.kernel
def gather(table: Table[Scalar], where: Index, y: Mutable[Scalar]):
y = table.at(where)
hawk.embedded.export(gather, work / "gather").report["indices"]
[{'node': 2,
'kind': 'table_read',
'status': 'clamped',
'reason': 'a runtime index into a runtime-length plane',
'length': 'lut_table_len'}]
A project that forbids unproven indices says so in the profile, and the export refuses instead:
try:
hawk.embedded.export(gather, work / "gather_strict",
profile=EmbeddedProfile(index_policy="refuse"))
except HawkError as err:
print(err)
print("anything written:", (work / "gather_strict").exists())
'gather': the C target refuses node 2 (table_read) under index.unproven: the index is not provably in range (a runtime index into a runtime-length plane); index with a static loop index or a literal, or export with index_policy='clamp'
anything written: False
Budgets. A cap on the worst-case loop trips per sample:
@hawk.kernel
def settle(x: Scalar, y: Mutable[Scalar]):
s = x
for _k in range(5000):
s = s * 0.5 + 1.0
y = s
try:
hawk.embedded.export(settle, work / "settle",
profile=EmbeddedProfile(max_trips=1000))
except HawkError as err:
print(err)
'settle': the C target refuses node loop3 (loop) under budget.trips: 5000 worst-case loop trips per sample exceed max_trips=1000 (loop3 runs 5000); shorten the range or raise the cap
Floating-point domain. Every sqrt, log, division and similar site
gets a sign verdict. sqrt of a squared norm or of 1 + x*x is provably
safe; sqrt of a raw input has no provable sign. The default records the
verdicts in the report; fp_domain="refuse" turns an unknown into a
refusal:
from hawk.math import sqrt
@hawk.kernel
def root(x: Scalar, y: Mutable[Scalar]):
y = sqrt(x)
print(hawk.embedded.export(root, work / "root").report["fp_domain"])
try:
hawk.embedded.export(root, work / "root_strict",
profile=EmbeddedProfile(fp_domain="refuse"))
except HawkError as err:
print(err)
[{'node': 1, 'op': 'sqrt', 'status': 'unknown', 'reason': 'sqrt needs a nonneg operand; its sign is unknown'}]
'root': the C target refuses node 1 (sqrt) under fp.domain: sqrt needs a nonneg operand; its sign is unknown; bound the operand into the domain (abs, a positive offset, clip) or export with fp_domain='record'
Unsupported features. Some features have no C spelling in this version, random draws among them. They are refused by name, with the alternative:
import hawk.math as hm
@hawk.kernel
def draw(seed: Index, counter: Index, y: Mutable[Scalar]):
y = hm.random.uniform(seed, counter)
try:
hawk.embedded.export(draw, work / "draw")
except HawkError as err:
print(err)
'draw': the C target refuses node 2 (random_uniform) under unsupported.random: a random draw lowers to aether's counter-based generator; no counter-based draw is built for C yet; draw in the caller and pass the values in as a plane
Through the build door#
c is also a build target beside host and cuda, so one call can
produce the host library and the C unit together. The C never enters the
eagle manifest:
import json
hawk.build([drag], work / "both", targets=("host", "c"))
manifest = json.loads((work / "both" / "manifest.json").read_text())
print(sorted(p.name for p in (work / "both").iterdir()))
print("exec_targets:", manifest["exec_targets"])
['.hawk_unit', 'drag.c', 'drag.cpp', 'drag.embedded.json', 'drag.h', 'drag.json', 'drag.so', 'manifest.json']
exec_targets: ['host']
A c-only build directory is source for an embedded build, not something
hawk can run, and hawk.load says so:
hawk.build([drag], work / "c_only", targets=("c",))
try:
hawk.load(work / "c_only", "drag")
except HawkError as err:
print(str(err).replace(str(work), "work"))
'drag' in work/c_only was built for the 'c' target only: it is a standalone C unit (<name>.c, <name>.h, <name>.embedded.json, see hawk.embedded) for an embedded build, not a host artifact hawk.load can run; build it with targets=('host',) to load it here
What just happened#
hawk.embedded.exportturned an ordinary kernel intodrag.canddrag.hwith a plain C ABI, plus a JSON report of budgets, interface, index sites, floating-point sites and the checks that ran.The C matched the host build byte for byte in float64 and float32, because both evaluate every fold in the same order with contraction off.
The entry validated its pointers and partition and returned a status.
The verify pass refused, by name and before writing anything, what a profile ruled out or the C target cannot build.
Try this#
Compile
drag.cwith-ffp-contract=faston a machine with fused multiply-add and compare again: the bits can change, which is why the header asks for contraction off.Add a
Terminatedmask to the kernel and read the header: the output plane becomesinoutand the caller must initialise it, because a masked sample keeps its previous value.Set
EmbeddedProfile(max_ops=10)ondragand read the refusal.