timfuz: handle zeros more concretely

Signed-off-by: John McMaster <johndmcmaster@gmail.com>
This commit is contained in:
John McMaster 2018-09-19 13:45:13 -07:00
parent c2c996c706
commit 06d47dcb5e
6 changed files with 101 additions and 105 deletions

View File

@ -6,36 +6,48 @@ from timfuz import Benchmark, loadc_Ads_bs, load_sub, Ads2bounds, corners2csv, c
def gen_flat(fns_in, sub_json, corner=None): def gen_flat(fns_in, sub_json, corner=None):
Ads, bs = loadc_Ads_bs(fns_in, ico=True) Ads, bs = loadc_Ads_bs(fns_in, ico=True)
bounds = Ads2bounds(Ads, bs) bounds = Ads2bounds(Ads, bs)
zeros = set() # Elements with zero delay assigned due to sub group
group_zeros = set()
# Elements with a concrete delay
nonzeros = set() nonzeros = set()
if corner:
zero_row = [None, None, None, None]
zero_row[corner_s2i[corner]] = 0
else:
zero_row = None
for bound_name, bound_bs in bounds.items(): for bound_name, bound_bs in bounds.items():
sub = sub_json['subs'].get(bound_name, None) sub = sub_json['subs'].get(bound_name, None)
if sub: if bound_name in sub_json['zero_names']:
if zero_row:
yield bound_name, 0
elif sub:
print('sub', sub)
# put entire delay into pivot # put entire delay into pivot
pivot = sub_json['pivots'][bound_name] pivot = sub_json['pivots'][bound_name]
assert pivot not in zeros assert pivot not in group_zeros
nonzeros.add(pivot) nonzeros.add(pivot)
non_pivot = set(sub.keys() - set([pivot])) non_pivot = set(sub.keys() - set([pivot]))
#for name in non_pivot: #for name in non_pivot:
# assert name not in nonzeros, (pivot, name, nonzeros) # assert name not in nonzeros, (pivot, name, nonzeros)
zeros.update(non_pivot) group_zeros.update(non_pivot)
yield pivot, bound_bs yield pivot, bound_bs
else: else:
nonzeros.add(bound_name) nonzeros.add(bound_name)
yield bound_name, bound_bs yield bound_name, bound_bs
# non-pivots can appear multiple times, but they should always be zero # non-pivots can appear multiple times, but they should always be zero
# however, due to substitution limitations, just warn # however, due to substitution limitations, just warn
violations = zeros.intersection(nonzeros) violations = group_zeros.intersection(nonzeros)
if len(violations): if len(violations):
print('WARNING: %s non-0 non-pivot' % (len(violations))) print('WARNING: %s non-0 non-pivot' % (len(violations)))
# XXX: how to best handle these? # XXX: how to best handle these?
# should they be fixed 0? # should they be fixed 0?
if corner: if zero_row:
zero_row = [None, None, None, None] print('zero_row', len(group_zeros), len(violations))
zero_row[corner_s2i[corner]] = 0 for zero in group_zeros - violations:
for zero in zeros - violations: print('zero', zero)
yield zero, zero_row yield zero, zero_row

View File

@ -9,6 +9,20 @@ import sympy
from collections import OrderedDict from collections import OrderedDict
from fractions import Fraction from fractions import Fraction
def rm_zero_cols(Ads, verbose=True):
removed = OrderedSet()
print('Removing ZERO elements')
for row_ds in Ads:
for k in set(row_ds.keys()):
if k in removed:
del row_ds[k]
elif k.find('ZERO') >= 0:
del row_ds[k]
removed.add(k)
if verbose:
print(' Removing %s' % k)
return removed
def fracr_quick(r): def fracr_quick(r):
return [Fraction(numerator=int(x), denominator=1) for x in r] return [Fraction(numerator=int(x), denominator=1) for x in r]
@ -20,14 +34,13 @@ def fracm_quick(m):
print('fracm_quick type: %s' % t) print('fracm_quick type: %s' % t)
return [fracr_quick(r) for r in m] return [fracr_quick(r) for r in m]
class State(object): class State(object):
def __init__(self, Ads, drop_names=[]): def __init__(self, Ads, zero_names=[]):
self.Ads = Ads self.Ads = Ads
self.names = index_names(self.Ads) self.names = index_names(self.Ads)
# known zero delay elements # known zero delay elements
self.drop_names = OrderedSet(drop_names) self.zero_names = OrderedSet(zero_names)
# active names in rows # active names in rows
# includes sub variables, excludes variables that have been substituted out # includes sub variables, excludes variables that have been substituted out
self.base_names = OrderedSet(self.names) self.base_names = OrderedSet(self.names)
@ -46,30 +59,34 @@ class State(object):
" Largest: %u" % max([len(x) for x in self.subs.values()])) " Largest: %u" % max([len(x) for x in self.subs.values()]))
print(" Rows: %u" % len(self.Ads)) print(" Rows: %u" % len(self.Ads))
print( print(
" Cols (in): %u" % (len(self.base_names) + len(self.drop_names))) " Cols (in): %u" % (len(self.base_names) + len(self.zero_names)))
print(" Cols (preprocessed): %u" % len(self.base_names)) print(" Cols (preprocessed): %u" % len(self.base_names))
print(" Drop names: %u" % len(self.drop_names)) print(" ZERO names: %u" % len(self.zero_names))
print(" Cols (out): %u" % len(self.names)) print(" Cols (out): %u" % len(self.names))
print(" Solvable vars: %u" % len(self.names & self.base_names)) print(" Solvable vars: %u" % len(self.names & self.base_names))
assert len(self.names) >= len(self.subs) assert len(self.names) >= len(self.subs)
@staticmethod @staticmethod
def load(fn_ins, simplify=False, corner=None): def load(fn_ins, simplify=False, corner=None, rm_zero=False):
zero_names = OrderedSet()
Ads, b = loadc_Ads_b(fn_ins, corner=corner, ico=True) Ads, b = loadc_Ads_b(fn_ins, corner=corner, ico=True)
if rm_zero:
zero_names = rm_zero_cols(Ads)
if simplify: if simplify:
print('Simplifying corner %s' % (corner, )) print('Simplifying corner %s' % (corner, ))
Ads, b = simplify_rows(Ads, b, remove_zd=False, corner=corner) Ads, b = simplify_rows(Ads, b, remove_zd=False, corner=corner)
return State(Ads) return State(Ads, zero_names=zero_names)
def write_state(state, fout): def write_state(state, fout):
j = { j = {
'names': 'names':
OrderedDict([(x, None) for x in state.names]), OrderedDict([(x, None) for x in state.names]),
'drop_names': 'zero_names':
list(state.drop_names), sorted(list(state.zero_names)),
'base_names': 'base_names':
list(state.base_names), sorted(list(state.base_names)),
'subs': 'subs':
OrderedDict([(name, values) for name, values in state.subs.items()]), OrderedDict([(name, values) for name, values in state.subs.items()]),
'pivots': 'pivots':
@ -172,11 +189,11 @@ def state_rref(state, verbose=False):
return state return state
def run(fnout, fn_ins, simplify=False, corner=None, verbose=0): def run(fnout, fn_ins, simplify=False, corner=None, rm_zero=False, verbose=0):
print('Loading data') print('Loading data')
assert len(fn_ins) > 0 assert len(fn_ins) > 0
state = State.load(fn_ins, simplify=simplify, corner=corner) state = State.load(fn_ins, simplify=simplify, corner=corner, rm_zero=rm_zero)
state_rref(state, verbose=verbose) state_rref(state, verbose=verbose)
state.print_stats() state.print_stats()
if fnout: if fnout:
@ -195,6 +212,7 @@ def main():
parser.add_argument('--verbose', action='store_true', help='') parser.add_argument('--verbose', action='store_true', help='')
parser.add_argument('--simplify', action='store_true', help='') parser.add_argument('--simplify', action='store_true', help='')
parser.add_argument('--corner', default="slow_max", help='') parser.add_argument('--corner', default="slow_max", help='')
parser.add_argument('--rm-zero', action='store_true', help='Remove ZERO elements')
parser.add_argument( parser.add_argument(
'--speed-json', '--speed-json',
default='build_speed/speed.json', default='build_speed/speed.json',
@ -214,6 +232,7 @@ def main():
fn_ins=fns_in, fn_ins=fns_in,
simplify=args.simplify, simplify=args.simplify,
corner=args.corner, corner=args.corner,
rm_zero=args.rm_zero,
verbose=args.verbose) verbose=args.verbose)
finally: finally:
print('Exiting after %s' % bench) print('Exiting after %s' % bench)

View File

@ -30,47 +30,6 @@ def mkestimate(Anp, b):
return x0 return x0
def save(outfn, xvals, names, corner):
# ballpark minimum actual observed delay is around 7 (carry chain)
# anything less than one is probably a solver artifact
delta = 0.5
corneri = corner_s2i[corner]
# Round conservatively
roundf = {
'fast_max': math.ceil,
'fast_min': math.floor,
'slow_max': math.ceil,
'slow_min': math.floor,
}[corner]
print('Writing results')
skips = 0
keeps = 0
with open(outfn, 'w') as fout:
# write as one variable per line
# this natively forms a bound if fed into linprog solver
fout.write('ico,fast_max fast_min slow_max slow_min,rows...\n')
for xval, name in zip(xvals, names):
row_ico = 1
# also review ceil vs floor choice for min vs max
# lets be more conservative for now
if xval < delta:
#print('Skipping %s: %0.6f' % (name, xval))
skips += 1
continue
keeps += 1
#xvali = round(xval)
items = [str(row_ico), acorner2csv(roundf(xval), corneri)]
items.append('%u %s' % (1, name))
fout.write(','.join(items) + '\n')
print(
'Wrote: skip %u => %u / %u valid delays' % (skips, keeps, len(names)))
assert keeps, 'Failed to estimate delay'
def run_corner( def run_corner(
Anp, b, names, corner, verbose=False, opts={}, meta={}, outfn=None): Anp, b, names, corner, verbose=False, opts={}, meta={}, outfn=None):
# Given timing scores for above delays (-ps) # Given timing scores for above delays (-ps)
@ -140,7 +99,7 @@ def run_corner(
print('Done') print('Done')
if outfn: if outfn:
save(outfn, res.x, names, corner) timfuz_solve.solve_save(outfn, res.x, names, corner, verbose=verbose)
def main(): def main():

View File

@ -12,50 +12,12 @@ import time
import timfuz_solve import timfuz_solve
def save(outfn, xvals, names, corner):
# ballpark minimum actual observed delay is around 7 (carry chain)
# anything less than one is probably a solver artifact
delta = 0.5
corneri = corner_s2i[corner]
roundf = {
'fast_max': math.ceil,
'fast_min': math.floor,
'slow_max': math.ceil,
'slow_min': math.floor,
}[corner]
print('Writing results')
zeros = 0
with open(outfn, 'w') as fout:
# write as one variable per line
# this natively forms a bound if fed into linprog solver
fout.write('ico,fast_max fast_min slow_max slow_min,rows...\n')
for xval, name in zip(xvals, names):
row_ico = 1
# FIXME: only report for the given corner?
# also review ceil vs floor choice for min vs max
# lets be more conservative for now
if xval < delta:
print('WARNING: near 0 delay on %s: %0.6f' % (name, xval))
zeros += 1
#continue
items = [str(row_ico), acorner2csv(roundf(xval), corneri)]
items.append('%u %s' % (1, name))
fout.write(','.join(items) + '\n')
nonzeros = len(names) - zeros
print(
'Wrote: %u / %u constrained delays, %u zeros' %
(nonzeros, len(names), zeros))
def run_corner( def run_corner(
Anp, b, names, corner, verbose=False, opts={}, meta={}, outfn=None): Anp, b, names, corner, verbose=False, opts={}, meta={}, outfn=None):
if len(Anp) == 0: if len(Anp) == 0:
print('WARNING: zero equations') print('WARNING: zero equations')
if outfn: if outfn:
save(outfn, [], [], corner) timfuz_solve.solve_save(outfn, [], [], corner)
return return
maxcorner = { maxcorner = {
'slow_max': True, 'slow_max': True,
@ -180,7 +142,7 @@ def run_corner(
print('Delay on %d / %d' % (nonzeros, len(res.x))) print('Delay on %d / %d' % (nonzeros, len(res.x)))
if outfn: if outfn:
save(outfn, res.x, names, corner) timfuz_solve.solve_save(outfn, res.x, names, corner, verbose=verbose)
def main(): def main():

View File

@ -107,6 +107,7 @@ corner_s2i = OrderedDict(
def allow_zero_eqns(): def allow_zero_eqns():
'''If true, allow a system of equations with no equations'''
return os.getenv('ALLOW_ZERO_EQN', 'N') == 'Y' return os.getenv('ALLOW_ZERO_EQN', 'N') == 'Y'
@ -732,7 +733,7 @@ def row_sub_vars(row, sub_json, strict=False, verbose=False):
print(row.items()) print(row.items())
delvars = 0 delvars = 0
for k in sub_json['drop_names']: for k in sub_json['zero_names']:
try: try:
del row[k] del row[k]
delvars += 1 delvars += 1
@ -908,3 +909,7 @@ def tilej_stats(tilej):
print( print(
' %s: %u / %u solved, %u / %u covered' % ' %s: %u / %u solved, %u / %u covered' %
(etype, solved, net, covered, net)) (etype, solved, net, covered, net))
def load_bounds(bounds_csv, corner, ico=True):
Ads, b = loadc_Ads_b([bounds_csv], corner, ico=ico)
return Ads2bounds(Ads, b)

View File

@ -1,9 +1,10 @@
#!/usr/bin/env python3 #!/usr/bin/env python3
from timfuz import simplify_rows, loadc_Ads_b, index_names, A_ds2np, run_sub_json, print_eqns, Ads2bounds, instances, SimplifiedToZero, allow_zero_eqns from timfuz import simplify_rows, loadc_Ads_b, index_names, A_ds2np, run_sub_json, print_eqns, Ads2bounds, instances, SimplifiedToZero, allow_zero_eqns, corner_s2i, acorner2csv
from timfuz_massage import massage_equations from timfuz_massage import massage_equations
import numpy as np import numpy as np
import sys import sys
import math
def check_feasible(A_ub, b_ub): def check_feasible(A_ub, b_ub):
@ -93,6 +94,44 @@ def filter_bounds(Ads, b, bounds, corner):
return ret_Ads, ret_b return ret_Ads, ret_b
def solve_save(outfn, xvals, names, corner, save_zero=True, verbose=False):
# ballpark minimum actual observed delay is around 7 (carry chain)
# anything less than one is probably a solver artifact
delta = 0.5
corneri = corner_s2i[corner]
roundf = {
'fast_max': math.ceil,
'fast_min': math.floor,
'slow_max': math.ceil,
'slow_min': math.floor,
}[corner]
print('Writing results')
zeros = 0
with open(outfn, 'w') as fout:
# write as one variable per line
# this natively forms a bound if fed into linprog solver
fout.write('ico,fast_max fast_min slow_max slow_min,rows...\n')
for xval, name in zip(xvals, names):
row_ico = 1
if xval < delta:
if verbose:
print('WARNING: near 0 delay on %s: %0.6f' % (name, xval))
zeros += 1
if not save_zero:
continue
items = [str(row_ico), acorner2csv(roundf(xval), corneri)]
items.append('%u %s' % (1, name))
fout.write(','.join(items) + '\n')
nonzeros = len(names) - zeros
print(
'Wrote: %u / %u constrained delays, %u zeros' %
(nonzeros, len(names), zeros))
assert nonzeros, 'Failed to estimate delay'
def run( def run(
fns_in, fns_in,
corner, corner,