float_aligned_quantize.py (8664B)
1 #!/usr/bin/env python3 2 """Combined near/far RNE with exact-rational IEEE-neighbor expectations.""" 3 import argparse 4 import hashlib 5 import json 6 from pathlib import Path 7 import random 8 import statistics 9 10 from float_quantize import ROOT, BIAS, INF, MAX, dyadic, value, encoded 11 from float_multiply import Runner, sha 12 from base_workloads import encode as nat 13 from http_headers import pair, tree_list, expect 14 15 16 def nearest(x): 17 assert x >= 0 18 if x >= value(MAX): 19 bits=INF if x >= (value(MAX)+dyadic(1,1024))/2 else MAX 20 else: 21 lo,hi=0,MAX 22 while lo+1 < hi: 23 mid=(lo+hi)//2 24 if value(mid) <= x: lo=mid 25 else: hi=mid 26 below,above=x-value(lo),value(hi)-x 27 bits=lo if below < above or (below==above and lo%2==0) else hi 28 inexact=bits==INF or value(bits)!=x 29 return bits,inexact,inexact and bits<2**52 30 31 32 def exact(row,subtract=False): 33 scale,gap,a,b=row 34 assert 3<=scale and 0<=gap<=4096 35 assert 2**52<=a<2**53 and 2**52<=b<2**53 36 assert gap or not subtract or a>=b 37 return dyadic(a,scale-BIAS)+(-1 if subtract else 1)*dyadic(b,scale-BIAS-gap) 38 39 40 def cases(): 41 lo,hi=2**52,2**53-1 42 pairs=[(lo,lo),(lo,lo+1),(lo,hi),(lo+1,lo),(lo+1,hi),(hi,lo),(hi,hi), 43 (3*2**51,lo),(hi,hi-1)] 44 scales=[3,1176,1177,1178,1229,1230,1231,2252,3274,3275,3276,4608] 45 rows=[(s,g,max(a,b) if g==0 else a,min(a,b) if g==0 else b) 46 for s in scales for g in [0,1,27,53,54,55,56,63,127,1074,2097] 47 for a,b in pairs if g>=55 or s>=g] 48 rng=random.Random(5518) 49 for _ in range(192): 50 s=rng.randrange(3,3400);g=rng.randrange(2098) 51 a,b=sorted([rng.randrange(lo,hi+1) for _ in range(2)],reverse=True) 52 if g>=55 or s>=g: rows.append((s,g,a,b)) 53 return rows 54 55 56 def raw_rows(rows): 57 return tree_list([pair(nat(s),pair(nat(g),pair(nat(a),nat(b)))) for s,g,a,b in rows]) 58 59 60 def main(): 61 p=argparse.ArgumentParser(description=__doc__) 62 p.add_argument('tricu',type=Path) 63 p.add_argument('--directory',required=True,type=Path) 64 args=p.parse_args() 65 root=args.directory.resolve();root.mkdir(parents=True,exist_ok=False) 66 work=root/'workspace';work.mkdir() 67 sources={'driver.tri':'bench/float-aligned-quantize.tri','fast.tri':'bench/float-quantize-fast.tri', 68 'quantize.tri':'bench/float-quantize.tri','pipelines.tri':'bench/float-pipelines.tri', 69 'kernels.tri':'bench/float-significands.tri','layouts.tri':'bench/float-layouts.tri', 70 'native_math.tri':'lib/math/native.tri'} 71 for name,path in sources.items(): (work/name).write_bytes((ROOT/path).read_bytes()) 72 report=dict(complete=False,scope='positive normalized magnitude RNE; trusted internal invariants', 73 runtime_sha256=sha(args.tricu),compiler_sha256=sha(ROOT/'bootstrap/build-stable.arboricx'), 74 harness_sha256=sha(Path(__file__)),sources={n:sha(ROOT/p) for n,p in sources.items()}, 75 validation=[],demand=[],samples=[],summaries=[]) 76 runner=Runner(args.tricu,root,1800,memory_mib=2048) 77 try: 78 tool=runner.imported(ROOT/'bootstrap/build-stable.arboricx','compiler');bundle=root/'aligned.arboricx' 79 runner.run('compile',['compile','--file',work/'driver.tri','--toolchain',tool,'--tool-store',runner.store, 80 '--store',runner.store,'--output',bundle,'--compile-timeout','240'],270) 81 pin=runner.imported(bundle,'aligned');report['bundle_sha256']=sha(bundle) 82 def run(label,name,rows,wanted,measure=False): 83 file=root/(label+'.input.tree');file.write_bytes(raw_rows(rows)) 84 actual=runner.invoke(label,pin,name,['--arg-tree-file',file]+(['--profile-full-result'] if measure else [])) 85 expect(actual,tree_list([encoded(x) for x in wanted]),label) 86 if not measure: 87 report['validation'].append(dict(label=label,cases=len(rows),input_sha256=sha(file), 88 output_sha256=hashlib.sha256(actual).hexdigest()));return 89 points={v['profile']:v for line in (root/(label+'.log')).read_text().splitlines() 90 if line.startswith('{') for v in [json.loads(line)]} 91 a,b=points['invoke-begin-1'],points['force-end-1'] 92 return dict(wall_ns=b['wall_ns']-a['wall_ns'],allocated_bytes=b['allocated_bytes']-a['allocated_bytes']) 93 rows=cases();report['cases_per_operation']=len(rows) 94 for name,sub in [('adds',False),('subtracts',True)]: 95 for offset in range(0,len(rows),24): 96 batch=rows[offset:offset+24] 97 run(f'check-{name}-{offset}',name,batch,[nearest(exact(x,sub)) for x in batch]) 98 far=[x for x in rows if x[1]>=55] 99 report['far_cases_per_surrogate']=len(far) 100 for name,sub in [('surrogateAdds',False),('surrogateSubtracts',True)]: 101 for offset in range(0,len(far),24): 102 batch=far[offset:offset+24] 103 run(f'check-{name}-{offset}',name,batch,[nearest(exact(x,sub)) for x in batch]) 104 # Materialize some far gaps in pure tricu as a separate exact control. 105 controls=[(2252,g,2**52+i,2**53-1-i) for g in [54,55,56,63,127] for i in range(4)] 106 for name,sub in [('exactAdds',False),('exactSubtracts',True)]: 107 run('check-'+name,name,controls,[nearest(exact(x,sub)) for x in controls]) 108 # Synthetic exact magnitudes exercise quantization beneath the binary64 grid. 109 bad=[(1177,55,2**52,2**52),(1178,55,3*2**51,2**52)] 110 run('discard-control','discardControl',bad,[(0,True,True),(2,True,True)]) 111 assert nearest(exact(bad[0],False))==(1,True,True) 112 assert nearest(exact(bad[1],True))==(1,True,True) 113 report['discard_counterexamples']=2 114 # Symbolic boundedness cases use the far-gap theorem for astronomical gaps. 115 huge=[(2252,2**128,2**52,2**53-1),(1177,2**128,2**52,2**52), 116 (1178,2**128,3*2**51,2**52)] 117 run('huge-add','adds',huge,[(0x3ff0000000000000,True,False),(1,True,True),(2,True,True)]) 118 run('huge-subtract','subtracts',huge,[(0x3ff0000000000000,True,False),(0,True,True),(1,True,True)]) 119 report['huge_cases']='six symbolic boundedness checks, not huge-integer oracle computations' 120 for name,wanted in [('farAddDemand',(1,True,True)),('farSubtractDemand',(1,True,True)), 121 ('cancellationDemand',(0,False,False)), 122 ('normalAddDemand',(0x3ff0000000000000,True,False)), 123 ('normalSubtractDemand',(0x3ff0000000000000,True,False)), 124 ('overflowDemand',(INF,True,False))]: 125 actual=runner.invoke('demand-'+name,pin,name,['--arg','0']);expect(actual,encoded(wanted),name) 126 report['demand'].append(dict(name=name,outcome='expected-result')) 127 groups={str(g):[(2252,g,2**52+i,2**53-1-i) for i in range(16)] for g in [54,55,127,2097,2**128]} 128 groups['underflow']=[(1177,55,2**52,2**52+i) for i in range(16)] 129 jobs=[] 130 for group,batch in groups.items(): 131 for name,sub in [('adds',False),('subtracts',True)]: 132 wanted=[nearest(exact(x,sub)) for x in batch] if group!=str(2**128) else [(0x3ff0000000000000+i,True,False) for i in range(16)] 133 jobs.append((group,name,batch,wanted)) 134 if group!='54': 135 jobs.append((group,'surrogateSubtracts' if sub else 'surrogateAdds',batch,wanted)) 136 if group in ['54','55','127']: 137 jobs.append((group,'exactSubtracts' if sub else 'exactAdds',batch,wanted)) 138 rng=random.Random(5518) 139 for rep in range(5): 140 schedule=list(jobs);rng.shuffle(schedule) 141 for group,name,batch,wanted in schedule: 142 sample=run(f'measure-{group}-{name}-{rep}',name,batch,wanted,True) 143 report['samples'].append(dict(group=group,name=name,size=len(batch),repeat=rep,warmup=rep==0,**sample)) 144 for group,name,batch,_ in jobs: 145 samples=[s for s in report['samples'] if s['group']==group and s['name']==name and not s['warmup']] 146 row=dict(group=group,name=name,size=len(batch)) 147 for key in ['wall_ns','allocated_bytes']: 148 row[key]=statistics.median(s[key] for s in samples) 149 row[key+'_min']=min(s[key] for s in samples);row[key+'_max']=max(s[key] for s in samples) 150 report['summaries'].append(row);print(json.dumps(row),flush=True) 151 report['complete']=True 152 finally: 153 (root/'report.json').write_text(json.dumps(report,indent=2)+'\n') 154 155 156 if __name__=='__main__': main()