float_ieee.py (10371B)
1 #!/usr/bin/env python3 2 """RNE four-operation IEEE-word policy, including five flags and raw transport.""" 3 import argparse 4 import hashlib 5 import json 6 from pathlib import Path 7 import random 8 import statistics 9 10 from float_aligned_quantize import nearest 11 from float_quantize import ROOT, dyadic, value 12 from float_multiply import Runner, sha 13 from base_workloads import encode as nat 14 from http_headers import LEAF, TRUE, pair, tree_list, expect 15 from float_finite import SIGN, LIMIT, MASK, finite_value, cases as add_cases 16 from float_finite_product_quotient import cases as product_cases 17 18 INF=0x7ff0000000000000 19 QNAN=0x7ff8000000000000 20 QUIET=1<<51 21 MIN_NORMAL=1<<52 22 TINY_BOUNDARY=value(MIN_NORMAL)-dyadic(1,-1076) 23 OPS=['adds','subtracts','multiplies','divides'] 24 25 26 def nan(w):return (w&MASK)>INF 27 28 def signaling(w):return nan(w) and not w&QUIET 29 30 def success(word,invalid=False,dz=False,of=False,uf=False,ix=False): 31 return True,(word,(invalid,dz,of,uf,ix)) 32 33 34 def oracle(a,b,op): 35 assert a>=0 and b>=0 36 if a>=LIMIT or b>=LIMIT:return False,2 37 if nan(a) or nan(b):return success((a if nan(a) else b)|QUIET,invalid=signaling(a) or signaling(b)) 38 ma,mb=a&MASK,b&MASK;sa,sb=bool(a&SIGN),bool(b&SIGN) 39 ia,ib=ma==INF,mb==INF;za,zb=ma==0,mb==0 40 invalid=lambda:success(QNAN,invalid=True) 41 signed_inf=lambda negative:INF|(SIGN if negative else 0) 42 if op in ['adds','subtracts']: 43 effective_b=sb != (op=='subtracts') 44 if ia or ib: 45 if ia and ib and sa!=effective_b:return invalid() 46 return success(signed_inf(sa if ia else effective_b)) 47 x=finite_value(a)+(-finite_value(b) if op=='subtracts' else finite_value(b)) 48 negative=x<0 if x else sa and effective_b 49 elif op=='multiplies': 50 if (ia and zb) or (ib and za):return invalid() 51 if ia or ib:return success(signed_inf(sa!=sb)) 52 x=finite_value(a)*finite_value(b);negative=sa!=sb 53 else: 54 assert op=='divides' 55 if (ia and ib) or (za and zb):return invalid() 56 if ia:return success(signed_inf(sa!=sb)) 57 if ib:return success(SIGN if sa!=sb else 0) 58 if zb:return success(signed_inf(sa!=sb),dz=True) 59 x=finite_value(a)/finite_value(b);negative=sa!=sb 60 bits,ix,_=nearest(abs(x)) 61 return success(bits|(SIGN if negative else 0),of=bits==INF, 62 uf=ix and abs(x)<TINY_BOUNDARY,ix=ix) 63 64 65 def encoded(reply): 66 ok,payload=reply 67 if not ok:return pair(LEAF,nat(payload)) 68 word,flags=payload 69 f=TRUE if flags[-1] else LEAF 70 for bit in reversed(flags[:-1]):f=pair(TRUE if bit else LEAF,f) 71 return pair(TRUE,pair(nat(word),f)) 72 73 74 def class_words(): 75 mag=[0,1,MIN_NORMAL,0x3ff0000000000000,0x7fefffffffffffff,INF, 76 QNAN,QNAN|1,INF|(2**52-1),INF|1,INF|(QUIET-1),INF|2**31] 77 return [w|sign for w in mag for sign in [0,SIGN]] 78 79 80 def boundary_pairs(): 81 a=(511<<52)|(((2**27-1)<<26)-2**52) 82 b=(512<<52)|(((2**27+1)<<25)-2**52) 83 pairs=[(a+i,b) for i in [-1,0,1]] 84 pairs += [(MIN_NORMAL,0x3fefffffffffffff),(0x001fffffffffffff,0x4000000000000000), 85 ((512<<52)|1,(511<<52)|(2**52-2))] 86 return [(x|sa,y|sb) for x,y in pairs for sa in [0,SIGN] for sb in [0,SIGN]] 87 88 89 def cases(op): 90 finite=add_cases() if op in ['adds','subtracts'] else product_cases() 91 words=class_words() 92 return list(dict.fromkeys(finite+[(a,b) for a in words for b in words]+boundary_pairs())) 93 94 95 def direct_cases(): 96 return [(s,((2**54-1)<<(1228-s))+delta) for s in [1224,1226,1228] 97 for delta in range(-18,19)] 98 99 100 def main(): 101 p=argparse.ArgumentParser(description=__doc__) 102 p.add_argument('tricu',type=Path);p.add_argument('--directory',required=True,type=Path) 103 args=p.parse_args();root=args.directory.resolve();root.mkdir(parents=True,exist_ok=False) 104 work=root/'workspace';work.mkdir() 105 sources={'driver.tri':'bench/float-ieee.tri','product_quotient.tri':'bench/float-finite-product-quotient.tri', 106 'finite.tri':'bench/float-finite.tri','adders.tri':'bench/float-adders.tri', 107 'multiply.tri':'bench/float-multiply.tri','near.tri':'bench/float-near-jam.tri', 108 'aligned.tri':'bench/float-aligned-quantize.tri','fast.tri':'bench/float-quantize-fast.tri', 109 'quantize.tri':'bench/float-quantize.tri','pipelines.tri':'bench/float-pipelines.tri', 110 'kernels.tri':'bench/float-significands.tri','layouts.tri':'bench/float-layouts.tri', 111 'native_math.tri':'lib/math/native.tri'} 112 for name,path in sources.items():(work/name).write_bytes((ROOT/path).read_bytes()) 113 report=dict(complete=False,scope='four basic RNE operations; agreed NaN policy; explicit IEEE flags; benchmark only', 114 runtime_sha256=sha(args.tricu),compiler_sha256=sha(ROOT/'bootstrap/build-stable.arboricx'), 115 harness_sha256=sha(Path(__file__)),sources={n:sha(ROOT/p) for n,p in sources.items()}, 116 validation=[],demand=[],samples=[],summaries=[],cases_per_operation={}) 117 runner=Runner(args.tricu,root,2400,memory_mib=2048) 118 try: 119 tool=runner.imported(ROOT/'bootstrap/build-stable.arboricx','compiler');bundle=root/'ieee.arboricx' 120 runner.run('compile',['compile','--file',work/'driver.tri','--toolchain',tool,'--tool-store',runner.store, 121 '--store',runner.store,'--output',bundle,'--compile-timeout','240'],270) 122 pin=runner.imported(bundle,'ieee');report['bundle_sha256']=sha(bundle) 123 def run(label,name,raw,wanted,count,measure=False): 124 file=root/(label+'.input.tree');file.write_bytes(raw) 125 actual=runner.invoke(label,pin,name,['--arg-tree-file',file]+(['--profile-full-result'] if measure else [])) 126 expect(actual,wanted,label) 127 if not measure: 128 report['validation'].append(dict(label=label,cases=count,input_sha256=sha(file), 129 output_sha256=hashlib.sha256(actual).hexdigest()));return 130 points={v['profile']:v for line in (root/(label+'.log')).read_text().splitlines() 131 if line.startswith('{') for v in [json.loads(line)]} 132 a,b=points['invoke-begin-1'],points['force-end-1'] 133 return dict(wall_ns=b['wall_ns']-a['wall_ns'],allocated_bytes=b['allocated_bytes']-a['allocated_bytes']) 134 def material(rows,op): 135 return tree_list([pair(nat(a),nat(b)) for a,b in rows]),tree_list([encoded(oracle(a,b,op)) for a,b in rows]) 136 for name in OPS: 137 rows=cases(name);report['cases_per_operation'][name]=len(rows) 138 for offset in range(0,len(rows),12): 139 batch=rows[offset:offset+12];raw,wanted=material(batch,name) 140 run(f'check-{name}-{offset}',name,raw,wanted,len(batch)) 141 for offset in range(0,len(direct_cases()),12): 142 batch=direct_cases()[offset:offset+12] 143 raw=tree_list([pair(nat(s),nat(n)) for s,n in batch]) 144 want=[] 145 for s,n in batch: 146 x=dyadic(n,s-2304);bits,ix,_=nearest(x) 147 want.append(encoded(success(bits,of=bits==INF,uf=ix and x<TINY_BOUNDARY,ix=ix))) 148 run('direct-'+str(offset),'quantized',raw,tree_list(want),len(batch)) 149 rng=random.Random(754) 150 words=class_words()+[rng.getrandbits(64) for _ in range(128)] 151 for offset in range(0,len(words),24): 152 batch=words[offset:offset+24];raw=tree_list([nat(w) for w in batch]) 153 run('transport-'+str(offset),'transport',raw,raw,len(batch)) 154 rejects=[(a,b) for a in [LIMIT,LIMIT+1,2**128] for b in [0,INF,QNAN,INF|1]] 155 rejects += [(b,a) for a,b in rejects] 156 for name in OPS: 157 raw,wanted=material(rejects,name);run('reject-'+name,name,raw,wanted,len(rejects)) 158 for name,wanted in [('rangeDemand',encoded((False,2))), 159 ('nanDemand',encoded(success(QNAN|1,invalid=True))), 160 ('nanWordDemand',nat(QNAN|1)), 161 ('signalingDemand',pair(nat(QNAN|1),pair(TRUE,pair(LEAF,pair(LEAF,pair(LEAF,LEAF))))))]: 162 actual=runner.invoke('demand-'+name,pin,name,['--arg','0']) 163 expect(actual,wanted,name);report['demand'].append(dict(name=name,outcome='expected-result')) 164 for name,a,b,op in [ 165 ('storedMultiplies',MIN_NORMAL,0x3fefffffffffffff,'multiplies'), 166 ('storedDivides',0x001fffffffffffff,0x4000000000000000,'divides')]: 167 wrong=success(MIN_NORMAL,ix=True);correct=oracle(a,b,op);assert wrong!=correct 168 run('negative-'+name,name,tree_list([pair(nat(a),nat(b))]),tree_list([encoded(wrong)]),1) 169 report.setdefault('historical_underflow_counterexamples',[]).append(dict(name=name,words=[a,b],correct=correct,wrong=wrong)) 170 rng=random.Random(754) 171 groups={ 172 'normal':[(0x3ff0000000000000|rng.getrandbits(52),0x3ff0000000000000|rng.getrandbits(52)) for _ in range(16)], 173 'tininess-boundary':[(MIN_NORMAL,0x3fefffffffffffff) for _ in range(16)], 174 'zero':[(SIGN,0) for _ in range(16)], 175 'infinity':[(INF|SIGN,INF) for _ in range(16)], 176 'nan':[(QNAN|1,INF|1|SIGN) for _ in range(16)]} 177 jobs=[] 178 for group,batch in groups.items(): 179 for name in OPS: 180 raw,wanted=material(batch,name);jobs.append((group,name,raw,wanted,len(batch))) 181 for rep in range(5): 182 schedule=list(jobs);rng.shuffle(schedule) 183 for group,name,raw,wanted,size in schedule: 184 sample=run(f'measure-{group}-{name}-{rep}',name,raw,wanted,size,True) 185 report['samples'].append(dict(group=group,name=name,size=size,repeat=rep,warmup=rep==0,**sample)) 186 for group,name,_,_,size in jobs: 187 samples=[s for s in report['samples'] if s['group']==group and s['name']==name and not s['warmup']] 188 row=dict(group=group,name=name,size=size) 189 for key in ['wall_ns','allocated_bytes']: 190 row[key]=statistics.median(s[key] for s in samples) 191 row[key+'_min']=min(s[key] for s in samples);row[key+'_max']=max(s[key] for s in samples) 192 report['summaries'].append(row);print(json.dumps(row),flush=True) 193 report['complete']=True 194 finally:(root/'report.json').write_text(json.dumps(report,indent=2)+'\n') 195 196 197 if __name__=='__main__':main()