float_alignment.py (6413B)
1 #!/usr/bin/env python3 2 """Bounded normalized alignment control; independent exact-integer RNE oracle.""" 3 import argparse 4 import hashlib 5 import json 6 from pathlib import Path 7 import random 8 import statistics 9 10 from float_multiply import Runner, sha 11 from base_workloads import encode as nat 12 from http_headers import LEAF, TRUE, pair, tree_list, expect 13 14 ROOT = Path(__file__).resolve().parent.parent 15 16 17 def exact_round(n, precision=53): 18 cut = max(0, n.bit_length() - precision) 19 q, remainder = divmod(n, 1 << cut) 20 twice = remainder * 2 21 if twice > (1 << cut) or (twice == (1 << cut) and q % 2): 22 q += 1 23 if q.bit_length() > precision: 24 q //= 2 25 cut += 1 26 return cut, q, bool(remainder) 27 28 29 def expected(a, b, gap, subtract=False): 30 assert 2**52 <= a < 2**53 and 2**52 <= b < 2**53 31 assert gap >= 0 and (not subtract or gap or a >= b) 32 # All actual binary64 exponent gaps use the independent exact oracle. 33 # Astronomical counts use the far-gap theorem as a boundedness probe. 34 if gap > 4096: 35 assert gap >= 55 36 return gap, a, True 37 return exact_round((a << gap) - b if subtract else (a << gap) + b) 38 39 40 def material(rows, subtract=False): 41 raw = tree_list([pair(nat(g), pair(nat(a), nat(b))) for a,b,g in rows]) 42 wanted = tree_list([pair(nat(c), pair(nat(m), TRUE if f else LEAF)) 43 for c,m,f in [expected(a,b,g,subtract) for a,b,g in rows]]) 44 return raw, wanted 45 46 47 def main(): 48 p = argparse.ArgumentParser(description=__doc__) 49 p.add_argument('tricu', type=Path) 50 p.add_argument('--directory', type=Path, required=True) 51 args = p.parse_args() 52 root = args.directory.resolve(); root.mkdir(parents=True, exist_ok=False) 53 work = root/'workspace'; work.mkdir() 54 sources = {'driver.tri':'bench/float-alignment.tri', 55 'pipelines.tri':'bench/float-pipelines.tri', 56 'kernels.tri':'bench/float-significands.tri', 57 'layouts.tri':'bench/float-layouts.tri', 'native_math.tri':'lib/math/native.tri'} 58 for name, path in sources.items(): 59 (work/name).write_bytes((ROOT/path).read_bytes()) 60 report = dict(complete=False, runtime_sha256=sha(args.tricu), 61 compiler_sha256=sha(ROOT/'bootstrap/build-stable.arboricx'), 62 harness_sha256=sha(Path(__file__)), 63 sources={n:sha(ROOT/p) for n,p in sources.items()}, 64 validation=[], demand=[], samples=[], summaries=[]) 65 runner = Runner(args.tricu, root, 1200, memory_mib=2048) 66 try: 67 compiler = runner.imported(ROOT/'bootstrap/build-stable.arboricx', 'compiler') 68 bundle = root/'alignment.arboricx' 69 runner.run('compile', ['compile', '--file', work/'driver.tri', '--toolchain', compiler, 70 '--tool-store', runner.store, '--store', runner.store, '--output', bundle, 71 '--compile-timeout', '240'], 270) 72 pin = runner.imported(bundle, 'alignment'); report['bundle_sha256'] = sha(bundle) 73 74 def run(label, name, rows, subtract=False, measure=False): 75 raw, wanted = material(rows, subtract) 76 file = root/(label+'.input.tree'); file.write_bytes(raw) 77 actual = runner.invoke(label, pin, name, ['--arg-tree-file', file] + 78 (['--profile-full-result'] if measure else [])) 79 expect(actual, wanted, label) 80 if not measure: 81 report['validation'].append(dict(label=label, cases=len(rows), 82 input_sha256=hashlib.sha256(raw).hexdigest(), output_sha256=hashlib.sha256(actual).hexdigest())) 83 return 84 points = {v['profile']:v for line in (root/(label+'.log')).read_text().splitlines() 85 if line.startswith('{') for v in [json.loads(line)]} 86 a,b = points['invoke-begin-1'],points['force-end-1'] 87 return dict(wall_ns=b['wall_ns']-a['wall_ns'], allocated_bytes=b['allocated_bytes']-a['allocated_bytes']) 88 89 lo,hi = 2**52,2**53-1 90 pairs = [(lo,lo),(lo,lo+1),(lo,hi),(lo+1,lo),(lo+1,hi), 91 (hi,lo),(hi,hi),(hi,hi-1),(lo+2,lo+1)] 92 gaps = list(range(58))+[63,64,127,1022,1074,2046,2097,2**128] 93 rows = [(max(a,b) if g == 0 else a, min(a,b) if g == 0 else b,g) 94 for a,b in pairs for g in gaps] 95 rng = random.Random(5355) 96 rows += [(max(a,b),min(a,b),rng.randrange(2098)) 97 for a,b in [(rng.randrange(lo,hi+1),rng.randrange(lo,hi+1)) for _ in range(128)]] 98 report['cases_per_operation'] = len(rows) 99 for subtract,name in [(False,'adds'),(True,'subtracts')]: 100 for offset in range(0,len(rows),32): 101 run(f'check-{name}-{offset}',name,rows[offset:offset+32],subtract) 102 for name in ['farAddDemand','farSubtractDemand']: 103 actual = runner.invoke('demand-'+name,pin,name,['--arg','0']) 104 expect(actual,nat(lo),name) 105 report['demand'].append(dict(name=name,outcome='expected-result',scope='trusted-normalized-input fast path')) 106 groups = {str(g):[(lo+i, hi-i, g) for i in range(16)] for g in [1,27,54,55,2097,2**128]} 107 jobs = [(group,name,sub,rep) for group in groups for name,sub in [('adds',False),('subtracts',True)] for rep in range(5)] 108 rng.shuffle(jobs) 109 for group,name,sub,rep in jobs: 110 sample = run(f'measure-{group}-{name}-{rep}',name,groups[group],sub,True) 111 report['samples'].append(dict(group=group,name=name,repeat=rep,warmup=rep==0,**sample)) 112 for group in groups: 113 for name in ['adds','subtracts']: 114 samples = [s for s in report['samples'] if s['group']==group and s['name']==name and not s['warmup']] 115 row = dict(group=group,name=name,size=16) 116 for key in ['wall_ns','allocated_bytes']: 117 row[key] = statistics.median(s[key] for s in samples) 118 row[key+'_min'] = min(s[key] for s in samples) 119 row[key+'_max'] = max(s[key] for s in samples) 120 report['summaries'].append(row) 121 report['complete'] = True 122 finally: 123 (root/'report.json').write_text(json.dumps(report,indent=2)+'\n') 124 print('PASS bounded alignment:',report['cases_per_operation'],'cases per operation; two demand controls; 60 timed batches') 125 126 127 if __name__ == '__main__': 128 main()