float_finite.py (8651B)
1 #!/usr/bin/env python3 2 """Finite signed binary64 add/subtract: IEEE words, exact rational 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_aligned_quantize import nearest 11 from float_quantize import ROOT, 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 16 SIGN=1 << 63 17 LIMIT=1 << 64 18 MASK=SIGN-1 19 20 21 def finite_value(bits): 22 assert 0<=bits<LIMIT and (bits & MASK)>>52<2047 23 v=value(bits & MASK) 24 return -v if bits & SIGN else v 25 26 27 def oracle(a,b,subtract=False): 28 if a>=LIMIT or b>=LIMIT: return False,2 29 if (a & MASK)>>52==2047 or (b & MASK)>>52==2047: return False,1 30 x=finite_value(a)+(-finite_value(b) if subtract else finite_value(b)) 31 if x==0: 32 negative=bool(a & SIGN) and (bool(b & SIGN) != subtract) 33 return True,(SIGN if negative else 0,False,False) 34 bits,inexact,underflow=nearest(abs(x)) 35 return True,(bits | (SIGN if x<0 else 0),inexact,underflow) 36 37 38 def encoded(reply): 39 ok,payload=reply 40 if not ok:return pair(LEAF,nat(payload)) 41 bits,inexact,underflow=payload 42 return pair(TRUE,pair(nat(bits),pair(TRUE if inexact else LEAF,TRUE if underflow else LEAF))) 43 44 45 def normalized(bits): 46 e=(bits & MASK)>>52;f=bits & (2**52-1) 47 assert e<2047 48 if e:return bool(bits & SIGN),e+1229,2**52+f 49 if not f:return bool(bits & SIGN),1230,0 50 pad=53-f.bit_length() 51 return bool(bits & SIGN),1230-pad,f << pad 52 53 54 def special_words(): 55 mag=[0,1,2,3,2**51-1,2**51,2**52-2,2**52-1,2**52,2**52+1,2**53-1, 56 0x3ca0000000000000,0x3cb0000000000000,0x3fefffffffffffff, 57 0x3ff0000000000000,0x3ff0000000000001,0x3ff0000000000002, 58 0x3fffffffffffffff,0x4000000000000000,0x7feffffffffffffe,0x7fefffffffffffff] 59 return [x | sign for x in mag for sign in [0,SIGN]] 60 61 62 def cases(): 63 special=special_words();rows=[(a,b) for a in special for b in special] 64 for gap in range(61): 65 for f in [0,1,2**52-1]: 66 a=0x3ff0000000000000;b=((1023-gap)<<52)|f 67 for sa in [0,SIGN]: 68 for sb in [0,SIGN]:rows += [(a|sa,b|sb),(b|sb,a|sa)] 69 rng=random.Random(64053) 70 def word():return (rng.randrange(2047)<<52)|rng.getrandbits(52)|(rng.randrange(2)<<63) 71 rows += [(word(),word()) for _ in range(384)] 72 for _ in range(128): 73 a=word();rows += [(a,a),(a,a^SIGN)] 74 return list(dict.fromkeys(rows)) 75 76 77 def main(): 78 p=argparse.ArgumentParser(description=__doc__) 79 p.add_argument('tricu',type=Path);p.add_argument('--directory',required=True,type=Path) 80 args=p.parse_args();root=args.directory.resolve();root.mkdir(parents=True,exist_ok=False) 81 work=root/'workspace';work.mkdir() 82 sources={'driver.tri':'bench/float-finite.tri','near.tri':'bench/float-near-jam.tri', 83 'aligned.tri':'bench/float-aligned-quantize.tri','fast.tri':'bench/float-quantize-fast.tri', 84 'quantize.tri':'bench/float-quantize.tri','pipelines.tri':'bench/float-pipelines.tri', 85 'kernels.tri':'bench/float-significands.tri','layouts.tri':'bench/float-layouts.tri', 86 'native_math.tri':'lib/math/native.tri'} 87 for name,path in sources.items():(work/name).write_bytes((ROOT/path).read_bytes()) 88 report=dict(complete=False,scope='finite signed RNE; exact IEEE-word test interface; rejects nonfinite inputs', 89 runtime_sha256=sha(args.tricu),compiler_sha256=sha(ROOT/'bootstrap/build-stable.arboricx'), 90 harness_sha256=sha(Path(__file__)),sources={n:sha(ROOT/p) for n,p in sources.items()}, 91 validation=[],demand=[],samples=[],summaries=[]) 92 runner=Runner(args.tricu,root,2400,memory_mib=2048) 93 try: 94 tool=runner.imported(ROOT/'bootstrap/build-stable.arboricx','compiler');bundle=root/'finite.arboricx' 95 runner.run('compile',['compile','--file',work/'driver.tri','--toolchain',tool,'--tool-store',runner.store, 96 '--store',runner.store,'--output',bundle,'--compile-timeout','240'],270) 97 pin=runner.imported(bundle,'finite');report['bundle_sha256']=sha(bundle) 98 def run(label,name,raw,wanted,count,measure=False): 99 file=root/(label+'.input.tree');file.write_bytes(raw) 100 actual=runner.invoke(label,pin,name,['--arg-tree-file',file]+(['--profile-full-result'] if measure else [])) 101 expect(actual,wanted,label) 102 if not measure: 103 report['validation'].append(dict(label=label,cases=count,input_sha256=sha(file), 104 output_sha256=hashlib.sha256(actual).hexdigest()));return 105 points={v['profile']:v for line in (root/(label+'.log')).read_text().splitlines() 106 if line.startswith('{') for v in [json.loads(line)]} 107 a,b=points['invoke-begin-1'],points['force-end-1'] 108 return dict(wall_ns=b['wall_ns']-a['wall_ns'],allocated_bytes=b['allocated_bytes']-a['allocated_bytes']) 109 def material(rows,sub): 110 return tree_list([pair(nat(a),nat(b)) for a,b in rows]),tree_list([encoded(oracle(a,b,sub)) for a,b in rows]) 111 rows=cases();report['finite_pairs']=len(rows) 112 for name,sub in [('adds',False),('subtracts',True)]: 113 for offset in range(0,len(rows),24): 114 batch=rows[offset:offset+24];raw,wanted=material(batch,sub) 115 run(f'check-{name}-{offset}',name,raw,wanted,len(batch)) 116 words=special_words()+[sign|2**k for sign in [0,SIGN] for k in range(52)] 117 report['decode_and_flip_words']=len(words) 118 for offset in range(0,len(words),24): 119 batch=words[offset:offset+24];raw=tree_list([nat(w) for w in batch]) 120 wanted=tree_list([pair(TRUE if sign else LEAF,pair(nat(scale),nat(m))) for sign,scale,m in map(normalized,batch)]) 121 run('decode-'+str(offset),'decoded',raw,wanted,len(batch)) 122 run('flip-'+str(offset),'flipped',raw,tree_list([nat(w^SIGN) for w in batch]),len(batch)) 123 bad=[0x7ff0000000000000,0xfff0000000000000,0x7ff8000000000001, 124 0xfff8000000000001,0x7ff0000000000001,0xfff0000000000001,LIMIT,LIMIT+1,2**128] 125 rejects=[(a,b) for a in bad for b in [0,SIGN,0x3ff0000000000000]] 126 rejects += [(b,a) for a,b in rejects]+[(bad[0],LIMIT),(LIMIT,bad[0])] 127 report['rejection_pairs']=len(rejects) 128 for name,sub in [('adds',False),('subtracts',True)]: 129 raw,wanted=material(rejects,sub);run('reject-'+name,name,raw,wanted,len(rejects)) 130 actual=runner.invoke('demand-range',pin,'rangeDemand',['--arg','0']) 131 expect(actual,encoded((False,2)),'range rejection ignores second operand') 132 report['demand'].append(dict(name='rangeDemand',outcome='expected-result')) 133 groups={ 134 'normal':[(0x3ff0000000000000+i,0x3fefffffffffffff-i) for i in range(16)], 135 'opposite-signs':[(0x3ff0000000000000+i,SIGN|0x3fefffffffffffff-i) for i in range(16)], 136 'cancellation':[(0xbff0000000000000+i,0xbff0000000000000+i) for i in range(16)], 137 'subnormal':[(SIGN|(2**52-1-i),2**51+i) for i in range(16)], 138 'far':[(SIGN|0x3ff0000000000000+i,1+i) for i in range(16)], 139 'zero':[(SIGN,0xbff0000000000000+i) for i in range(16)], 140 'overflow':[(0x7fefffffffffffff-i,0x7fefffffffffffff-i) for i in range(16)]} 141 jobs=[] 142 for group,batch in groups.items(): 143 for name,sub in [('adds',False),('subtracts',True)]: 144 raw,wanted=material(batch,sub);jobs.append((group,name,raw,wanted,len(batch))) 145 rng=random.Random(64053) 146 for rep in range(5): 147 schedule=list(jobs);rng.shuffle(schedule) 148 for group,name,raw,wanted,size in schedule: 149 sample=run(f'measure-{group}-{name}-{rep}',name,raw,wanted,size,True) 150 report['samples'].append(dict(group=group,name=name,size=size,repeat=rep,warmup=rep==0,**sample)) 151 for group,name,_,_,size in jobs: 152 samples=[s for s in report['samples'] if s['group']==group and s['name']==name and not s['warmup']] 153 row=dict(group=group,name=name,size=size) 154 for key in ['wall_ns','allocated_bytes']: 155 row[key]=statistics.median(s[key] for s in samples) 156 row[key+'_min']=min(s[key] for s in samples);row[key+'_max']=max(s[key] for s in samples) 157 report['summaries'].append(row);print(json.dumps(row),flush=True) 158 report['complete']=True 159 finally:(root/'report.json').write_text(json.dumps(report,indent=2)+'\n') 160 161 162 if __name__=='__main__':main()