perm filename BOYER.TIM[TIM,LSP]17 blob sn#768060 filedate 1984-09-12 generic text, type C, neo UTF8

COMMENT ⊗ VALID 00031 PAGES C REC PAGE DESCRIPTION C00001 00001 C00003 00002 Comparison of LISPS C00005 00003 The ELISP code C00026 00004 (FILECREATED " 5-Jul-82 12:52:49" <CL.BOYER.LISPS>IREWRITE..4 14918 C00051 00005 The Maclisp Code C00072 00006 The ELISP test C00073 00007 Interlisp bcompl blocklib swap and noswap C00076 00008 Interlisp bcompl no blocklib swap and noswap C00080 00009 Maclisp C00086 00010 Interlisp (Dolphin and Dorado) C00117 00011 The INTERLISP VAX test C00120 00012 SAIL C00122 00013 SAIL (FIXSW T) C00125 00014 Boyer C00126 00015 NIL C00128 00016 FRANZ C00138 00017 SCORE Oct 18, 1983 C00140 00018 DEC780CL C00141 00019 InterLisp Vax 780 C00142 00020 PSL-20 3.3 C00143 00021 PSL-cray 3.2 C00145 00022 PSL-750 3.2 C00146 00023 PSL-780 3.2 C00147 00024 PSL-dn600 C00148 00025 PSL-dn300 C00149 00026 PSL-dn160 C00150 00027 PERQ 6/18/84 C00151 00028 PSL Numbers 7/31/84 C00152 00029 LMI/Tyson 15-Aug-84 1920 C00153 00030 S-1 August 21, 1984 C00154 00031 3600 Sept 12, 1984 C00155 ENDMK C⊗; Comparison of LISPS This page contains a summary. Subsequent pages contain the code used and documentation of the tests. All the code was compiled. Non GC time (seconds) GC time Total MACLISP (2060) 8.5 5.3 13.8 UCILISP (2060, (nouuo nil)) 9.3 4.7 14 INTERLISP (bcompl, blklib, swap, 2060) 11 6 17 ELISP (2060) 11 7 18 INTERLISP (bcompl, blklib, noswap, 2060) 11 7.5 18.5 INTERLISP (Dorado, bcompl, blklib) 18 11 29 INTERLISP (bcompl, no blklib, noswap, 2060) 39 7 46 INTERLISP (bcompl, no blklib, swap, 2060) 64 6 70 INTERLISP (VAX-780) 80 3 83 ZETALISP (LM-2, 1meg, gc-on) breakdown not available 97 INTERLISP (Dolphin, 1meg, bcompl, blklib) 132 35 167 The ELISP code (DECLARE (SPECIAL UNIFY-SUBST TEMP-TEMP)) (DE ADD-LEMMA (TERM) (COND ((AND (NOT (ATOM TERM)) (EQ (CAR TERM) (QUOTE EQUAL)) (NOT (ATOM (CADR TERM)))) (PUTPROP (CAR (CADR TERM)) (CONS TERM (GET (CAR (CADR TERM)) (QUOTE LEMMAS))) (QUOTE LEMMAS))) (T (ERROR (LIST (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM) TERM) )))) (DE ADD-LEMMA-LST (LST) (COND ((NULL LST) T) (T (ADD-LEMMA (CAR LST)) (ADD-LEMMA-LST (CDR LST))))) (DE APPLY-SUBST (ALIST TERM) (COND ((ATOM TERM) (COND ((SETQ TEMP-TEMP (ASSOC TERM ALIST)) (CDR TEMP-TEMP)) (T TERM))) (T (CONS (CAR TERM) (APPLY-SUBST-LST ALIST (CDR TERM)))))) (DE APPLY-SUBST-LST (ALIST LST) (COND ((NULL LST) NIL) (T (CONS (APPLY-SUBST ALIST (CAR LST)) (APPLY-SUBST-LST ALIST (CDR LST)))))) (DE FALSEP (X LST) (OR (EQUAL X (QUOTE (F))) (MEMBER X LST))) (DE ONE-WAY-UNIFY (TERM1 TERM2) (PROGN (SETQ UNIFY-SUBST NIL) (ONE-WAY-UNIFY1 TERM1 TERM2))) (DE ONE-WAY-UNIFY1 (TERM1 TERM2) (COND ((ATOM TERM2) (COND ((SETQ TEMP-TEMP (ASSOC TERM2 UNIFY-SUBST)) (EQUAL TERM1 (CDR TEMP-TEMP))) (T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1) UNIFY-SUBST)) T))) ((ATOM TERM1) NIL) ((EQ (CAR TERM1) (CAR TERM2)) (ONE-WAY-UNIFY1-LST (CDR TERM1) (CDR TERM2))) (T NIL))) (DE ONE-WAY-UNIFY1-LST (LST1 LST2) (COND ((NULL LST1) T) ((ONE-WAY-UNIFY1 (CAR LST1) (CAR LST2)) (ONE-WAY-UNIFY1-LST (CDR LST1) (CDR LST2))) (T NIL))) (DE REWRITE (TERM) (COND ((ATOM TERM) TERM) (T (REWRITE-WITH-LEMMAS (CONS (CAR TERM) (REWRITE-ARGS (CDR TERM))) (GET (CAR TERM) (QUOTE LEMMAS)))))) (DE REWRITE-ARGS (LST) (COND ((NULL LST) NIL) (T (CONS (REWRITE (CAR LST)) (REWRITE-ARGS (CDR LST)))))) (DE REWRITE-WITH-LEMMAS (TERM LST) (COND ((NULL LST) TERM) ((ONE-WAY-UNIFY TERM (CADR (CAR LST))) (REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST))))) (T (REWRITE-WITH-LEMMAS TERM (CDR LST))))) (DE SETUP NIL (ADD-LEMMA-LST (QUOTE ((EQUAL (COMPILE FORM) (REVERSE (CODEGEN (OPTIMIZE FORM) (NIL)))) (EQUAL (EQP X Y) (EQUAL (FIX X) (FIX Y))) (EQUAL (GREATERP X Y) (LESSP Y X)) (EQUAL (LESSEQP X Y) (NOT (LESSP Y X))) (EQUAL (GREATEREQP X Y) (NOT (LESSP X Y))) (EQUAL (BOOLEAN X) (OR (EQUAL X (T)) (EQUAL X (F)))) (EQUAL (IFF X Y) (AND (IMPLIES X Y) (IMPLIES Y X))) (EQUAL (EVEN1 X) (IF (ZEROP X) (T) (ODD (SUB1 X)))) (EQUAL (COUNTPS- L PRED) (COUNTPS-LOOP L PRED (ZERO))) (EQUAL (FACT- I) (FACT-LOOP I 1)) (EQUAL (REVERSE- X) (REVERSE-LOOP X (NIL))) (EQUAL (DIVIDES X Y) (ZEROP (REMAINDER Y X))) (EQUAL (ASSUME-TRUE VAR ALIST) (CONS (CONS VAR (T)) ALIST)) (EQUAL (ASSUME-FALSE VAR ALIST) (CONS (CONS VAR (F)) ALIST)) (EQUAL (TAUTOLOGY-CHECKER X) (TAUTOLOGYP (NORMALIZE X) (NIL))) (EQUAL (FALSIFY X) (FALSIFY1 (NORMALIZE X) (NIL))) (EQUAL (PRIME X) (AND (NOT (ZEROP X)) (NOT (EQUAL X (ADD1 (ZERO)))) (PRIME1 X (SUB1 X)))) (EQUAL (AND P Q) (IF P (IF Q (T) (F)) (F))) (EQUAL (OR P Q) (IF P (T) (IF Q (T) (F)) (F))) (EQUAL (NOT P) (IF P (F) (T))) (EQUAL (IMPLIES P Q) (IF P (IF Q (T) (F)) (T))) (EQUAL (FIX X) (IF (NUMBERP X) X (ZERO))) (EQUAL (IF (IF A B C) D E) (IF A (IF B D E) (IF C D E))) (EQUAL (ZEROP X) (OR (EQUAL X (ZERO)) (NOT (NUMBERP X)))) (EQUAL (PLUS (PLUS X Y) Z) (PLUS X (PLUS Y Z))) (EQUAL (EQUAL (PLUS A B) (ZERO)) (AND (ZEROP A) (ZEROP B))) (EQUAL (DIFFERENCE X X) (ZERO)) (EQUAL (EQUAL (PLUS A B) (PLUS A C)) (EQUAL (FIX B) (FIX C))) (EQUAL (EQUAL (ZERO) (DIFFERENCE X Y)) (NOT (LESSP Y X))) (EQUAL (EQUAL X (DIFFERENCE X Y)) (AND (NUMBERP X) (OR (EQUAL X (ZERO)) (ZEROP Y)))) (EQUAL (MEANING (PLUS-TREE (APPEND X Y)) A) (PLUS (MEANING (PLUS-TREE X) A) (MEANING (PLUS-TREE Y) A))) (EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X)) A) (FIX (MEANING X A))) (EQUAL (APPEND (APPEND X Y) Z) (APPEND X (APPEND Y Z))) (EQUAL (REVERSE (APPEND A B)) (APPEND (REVERSE B) (REVERSE A))) (EQUAL (TIMES X (PLUS Y Z)) (PLUS (TIMES X Y) (TIMES X Z))) (EQUAL (TIMES (TIMES X Y) Z) (TIMES X (TIMES Y Z))) (EQUAL (EQUAL (TIMES X Y) (ZERO)) (OR (ZEROP X) (ZEROP Y))) (EQUAL (EXEC (APPEND X Y) PDS ENVRN) (EXEC Y (EXEC X PDS ENVRN) ENVRN)) (EQUAL (MC-FLATTEN X Y) (APPEND (FLATTEN X) Y)) (EQUAL (MEMBER X (APPEND A B)) (OR (MEMBER X A) (MEMBER X B))) (EQUAL (MEMBER X (REVERSE Y)) (MEMBER X Y)) (EQUAL (LENGTH (REVERSE X)) (LENGTH X)) (EQUAL (MEMBER A (INTERSECT B C)) (AND (MEMBER A B) (MEMBER A C))) (EQUAL (NTH (ZERO) I) (ZERO)) (EQUAL (EXP I (PLUS J K)) (TIMES (EXP I J) (EXP I K))) (EQUAL (EXP I (TIMES J K)) (EXP (EXP I J) K)) (EQUAL (REVERSE-LOOP X Y) (APPEND (REVERSE X) Y)) (EQUAL (REVERSE-LOOP X (NIL)) (REVERSE X)) (EQUAL (COUNT-LIST Z (SORT-LP X Y)) (PLUS (COUNT-LIST Z X) (COUNT-LIST Z Y))) (EQUAL (EQUAL (APPEND A B) (APPEND A C)) (EQUAL B C)) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) (FIX X)) (EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE) BASE) (PLUS (POWER-EVAL L BASE) I)) (EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE) BASE) (PLUS I (PLUS (POWER-EVAL X BASE) (POWER-EVAL Y BASE)))) (EQUAL (REMAINDER Y 1) (ZERO)) (EQUAL (LESSP (REMAINDER X Y) Y) (NOT (ZEROP Y))) (EQUAL (REMAINDER X X) (ZERO)) (EQUAL (LESSP (QUOTIENT I J) I) (AND (NOT (ZEROP I)) (OR (ZEROP J) (NOT (EQUAL J 1))))) (EQUAL (LESSP (REMAINDER X Y) X) (AND (NOT (ZEROP Y)) (NOT (ZEROP X)) (NOT (LESSP X Y)))) (EQUAL (POWER-EVAL (POWER-REP I BASE) BASE) (FIX I)) (EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE) (POWER-REP J BASE) (ZERO) BASE) BASE) (PLUS I J)) (EQUAL (GCD X Y) (GCD Y X)) (EQUAL (NTH (APPEND A B) I) (APPEND (NTH A I) (NTH B (DIFFERENCE I (LENGTH A))))) (EQUAL (DIFFERENCE (PLUS X Y) X) (FIX Y)) (EQUAL (DIFFERENCE (PLUS Y X) X) (FIX Y)) (EQUAL (DIFFERENCE (PLUS X Y) (PLUS X Z)) (DIFFERENCE Y Z)) (EQUAL (TIMES X (DIFFERENCE C W)) (DIFFERENCE (TIMES C X) (TIMES W X))) (EQUAL (REMAINDER (TIMES X Z) Z) (ZERO)) (EQUAL (DIFFERENCE (PLUS B (PLUS A C)) A) (PLUS B C)) (EQUAL (DIFFERENCE (ADD1 (PLUS Y Z)) Z) (ADD1 Y)) (EQUAL (LESSP (PLUS X Y) (PLUS X Z)) (LESSP Y Z)) (EQUAL (LESSP (TIMES X Z) (TIMES Y Z)) (AND (NOT (ZEROP Z)) (LESSP X Y))) (EQUAL (LESSP Y (PLUS X Y)) (NOT (ZEROP X))) (EQUAL (GCD (TIMES X Z) (TIMES Y Z)) (TIMES Z (GCD X Y))) (EQUAL (VALUE (NORMALIZE X) A) (VALUE X A)) (EQUAL (EQUAL (FLATTEN X) (CONS Y (NIL))) (AND (NLISTP X) (EQUAL X Y))) (EQUAL (LISTP (GOPHER X)) (LISTP X)) (EQUAL (SAMEFRINGE X Y) (EQUAL (FLATTEN X) (FLATTEN Y))) (EQUAL (EQUAL (GREATEST-FACTOR X Y) (ZERO)) (AND (OR (ZEROP Y) (EQUAL Y 1)) (EQUAL X (ZERO)))) (EQUAL (EQUAL (GREATEST-FACTOR X Y) 1) (EQUAL X 1)) (EQUAL (NUMBERP (GREATEST-FACTOR X Y)) (NOT (AND (OR (ZEROP Y) (EQUAL Y 1)) (NOT (NUMBERP X))))) (EQUAL (TIMES-LIST (APPEND X Y)) (TIMES (TIMES-LIST X) (TIMES-LIST Y))) (EQUAL (PRIME-LIST (APPEND X Y)) (AND (PRIME-LIST X) (PRIME-LIST Y))) (EQUAL (EQUAL Z (TIMES W Z)) (AND (NUMBERP Z) (OR (EQUAL Z (ZERO)) (EQUAL W 1)))) (EQUAL (GREATEREQPR X Y) (NOT (LESSP X Y))) (EQUAL (EQUAL X (TIMES X Y)) (OR (EQUAL X (ZERO)) (AND (NUMBERP X) (EQUAL Y 1)))) (EQUAL (REMAINDER (TIMES Y X) Y) (ZERO)) (EQUAL (EQUAL (TIMES A B) 1) (AND (NOT (EQUAL A (ZERO))) (NOT (EQUAL B (ZERO))) (NUMBERP A) (NUMBERP B) (EQUAL (SUB1 A) (ZERO)) (EQUAL (SUB1 B) (ZERO)))) (EQUAL (LESSP (LENGTH (DELETE X L)) (LENGTH L)) (MEMBER X L)) (EQUAL (SORT2 (DELETE X L)) (DELETE X (SORT2 L))) (EQUAL (DSORT X) (SORT2 X)) (EQUAL (LENGTH (CONS X1 (CONS X2 (CONS X3 (CONS X4 (CONS X5 (CONS X6 X7))))))) (PLUS 6 (LENGTH X7))) (EQUAL (DIFFERENCE (ADD1 (ADD1 X)) 2) (FIX X)) (EQUAL (QUOTIENT (PLUS X (PLUS X Y)) 2) (PLUS X (QUOTIENT Y 2))) (EQUAL (SIGMA (ZERO) I) (QUOTIENT (TIMES I (ADD1 I)) 2)) (EQUAL (PLUS X (ADD1 Y)) (IF (NUMBERP Y) (ADD1 (PLUS X Y)) (ADD1 X))) (EQUAL (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y)) (IF (LESSP X Y) (NOT (LESSP Y Z)) (IF (LESSP Z Y) (NOT (LESSP Y X)) (EQUAL (FIX X) (FIX Z))))) (EQUAL (MEANING (PLUS-TREE (DELETE X Y)) A) (IF (MEMBER X Y) (DIFFERENCE (MEANING (PLUS-TREE Y) A) (MEANING X A)) (MEANING (PLUS-TREE Y) A))) (EQUAL (TIMES X (ADD1 Y)) (IF (NUMBERP Y) (PLUS X (TIMES X Y)) (FIX X))) (EQUAL (NTH (NIL) I) (IF (ZEROP I) (NIL) (ZERO))) (EQUAL (LAST (APPEND A B)) (IF (LISTP B) (LAST B) (IF (LISTP A) (CONS (CAR (LAST A)) B) B))) (EQUAL (EQUAL (LESSP X Y) Z) (IF (LESSP X Y) (EQUAL T Z) (EQUAL F Z))) (EQUAL (ASSIGNMENT X (APPEND A B)) (IF (ASSIGNEDP X A) (ASSIGNMENT X A) (ASSIGNMENT X B))) (EQUAL (CAR (GOPHER X)) (IF (LISTP X) (CAR (FLATTEN X)) (ZERO))) (EQUAL (FLATTEN (CDR (GOPHER X))) (IF (LISTP X) (CDR (FLATTEN X)) (CONS (ZERO) (NIL)))) (EQUAL (QUOTIENT (TIMES Y X) Y) (IF (ZEROP Y) (ZERO) (FIX X))) (EQUAL (GET J (SET I VAL MEM)) (IF (EQP J I) VAL (GET J MEM))))))) (DE TAUTOLOGYP (X TRUE-LST FALSE-LST) (COND ((TRUEP X TRUE-LST) T) ((FALSEP X FALSE-LST) NIL) ((ATOM X) NIL) ((EQ (CAR X) (QUOTE IF)) (COND ((TRUEP (CADR X) TRUE-LST) (TAUTOLOGYP (CADDR X) TRUE-LST FALSE-LST)) ((FALSEP (CADR X) FALSE-LST) (TAUTOLOGYP (CADDDR X) TRUE-LST FALSE-LST)) (T (AND (TAUTOLOGYP (CADDR X) (CONS (CADR X) TRUE-LST) FALSE-LST) (TAUTOLOGYP (CADDDR X) TRUE-LST (CONS (CADR X) FALSE-LST)))))) (T NIL))) (DE TAUTP (X) (TAUTOLOGYP (REWRITE X) NIL NIL)) (DE TEST NIL (TIMER (TEST1))) (DE TEST1 NIL (PROG (TERM ANS) (SETQ TERM (APPLY-SUBST (QUOTE ((X F (PLUS (PLUS A B) (PLUS C (ZERO)))) (Y F (TIMES (TIMES A B) (PLUS C D))) (Z F (REVERSE (APPEND (APPEND A B) (NIL)))) (U EQUAL (PLUS A B) (DIFFERENCE X Y)) (W LESSP (REMAINDER A B) (MEMBER A (LENGTH B))))) (QUOTE (IMPLIES (AND (IMPLIES X Y) (AND (IMPLIES Y Z) (AND (IMPLIES Z U) (IMPLIES U W)))) (IMPLIES X W))))) (SETQ ANS (TAUTP TERM)) (RETURN (LIST ANS)))) (DE TRANS-OF-IMPLIES (N) (LIST (QUOTE IMPLIES) (TRANS-OF-IMPLIES1 N) (LIST (QUOTE IMPLIES) 0 N))) (DE TRANS-OF-IMPLIES1 (N) (COND ((EQUAL N 1) (LIST (QUOTE IMPLIES) 0 1)) (T (LIST (QUOTE AND) (LIST (QUOTE IMPLIES) (SUB1 N) N) (TRANS-OF-IMPLIES1 (SUB1 N)))))) (DE TRUEP (X LST) (OR (EQUAL X (QUOTE (T))) (MEMBER X LST))) (FILECREATED " 5-Jul-82 12:52:49" <CL.BOYER.LISPS>IREWRITE..4 14918 changes to: IREWRITECOMS previous date: " 5-Jul-82 12:11:22" <CL.BOYER.LISPS>IREWRITE..3) (PRETTYCOMPRINT IREWRITECOMS) (RPAQQ IREWRITECOMS ((FNS * IREWRITEFNS) (PROP BLKLIBRARYDEF MEMBER) (BLOCKS (REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES TEST SETUP) (BLKLIBRARY EQUAL MEMBER GETPROP) (GLOBALVARS TEMP-TEMP UNIFY-SUBST))))) (RPAQQ IREWRITEFNS (ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP)) (DEFINEQ (ADD-LEMMA (LAMBDA (TERM) (COND ((AND (NOT (ATOM TERM)) (EQ (CAR TERM) (QUOTE EQUAL)) (NOT (ATOM (CADR TERM)))) (COND ((GETPROP (CAR (CADR TERM)) (QUOTE LEMMAS)) (PUTPROP (CAR (CADR TERM)) (QUOTE LEMMAS) (CONS TERM (GETPROP (CAR (CADR TERM)) (QUOTE LEMMAS))))) (T (SETPROPLIST (CAR (CADR TERM)) (CONS (QUOTE LEMMAS) (CONS (LIST TERM) (GETPROPLIST (CAR (CADR TERM)))))) ))) (T (ERROR (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM) TERM))))) (ADD-LEMMA-LST (LAMBDA (LST) (COND ((NULL LST) T) (T (ADD-LEMMA (CAR LST)) (ADD-LEMMA-LST (CDR LST)))))) (APPLY-SUBST (LAMBDA (ALIST TERM) (COND ((NLISTP TERM) (COND ((SETQ TEMP-TEMP (FASSOC TERM ALIST)) (CDR TEMP-TEMP)) (T TERM))) (T (CONS (CAR TERM) (APPLY-SUBST-LST ALIST (CDR TERM))))))) (APPLY-SUBST-LST (LAMBDA (ALIST LST) (COND ((NULL LST) NIL) (T (CONS (APPLY-SUBST ALIST (CAR LST)) (APPLY-SUBST-LST ALIST (CDR LST))))))) (FALSEP (LAMBDA (X LST) (OR (EQUAL X (QUOTE (F))) (MEMBER X LST)))) (ONE-WAY-UNIFY (LAMBDA (TERM1 TERM2) (PROGN (SETQ UNIFY-SUBST NIL) (ONE-WAY-UNIFY1 TERM1 TERM2)))) (ONE-WAY-UNIFY1 (LAMBDA (TERM1 TERM2) (COND ((NLISTP TERM2) (COND ((SETQ TEMP-TEMP (FASSOC TERM2 UNIFY-SUBST)) (EQUAL TERM1 (CDR TEMP-TEMP))) (T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1) UNIFY-SUBST)) T))) ((ATOM TERM1) NIL) ((EQ (CAR TERM1) (CAR TERM2)) (ONE-WAY-UNIFY1-LST (CDR TERM1) (CDR TERM2))) (T NIL)))) (ONE-WAY-UNIFY1-LST (LAMBDA (LST1 LST2) (COND ((NULL LST1) T) ((ONE-WAY-UNIFY1 (CAR LST1) (CAR LST2)) (ONE-WAY-UNIFY1-LST (CDR LST1) (CDR LST2))) (T NIL)))) (PTIME (LAMBDA NIL (PROG (GCTM) (SETQ GCTM (CLOCK 3)) (RETURN (CONS (IPLUS (CLOCK 2) GCTM) GCTM))))) (REWRITE (LAMBDA (TERM) (COND ((NLISTP TERM) TERM) (T (REWRITE-WITH-LEMMAS (CONS (CAR TERM) (REWRITE-ARGS (CDR TERM))) (GETPROP (CAR TERM) (QUOTE LEMMAS))))))) (REWRITE-ARGS (LAMBDA (LST) (COND ((NULL LST) NIL) (T (CONS (REWRITE (CAR LST)) (REWRITE-ARGS (CDR LST))))))) (REWRITE-WITH-LEMMAS (LAMBDA (TERM LST) (COND ((NULL LST) TERM) ((ONE-WAY-UNIFY TERM (CADR (CAR LST))) (REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST))))) (T (REWRITE-WITH-LEMMAS TERM (CDR LST)))))) (SETUP (LAMBDA NIL (ADD-LEMMA-LST (QUOTE ((EQUAL (COMPILE FORM) (REVERSE (CODEGEN (OPTIMIZE FORM) (NIL)))) (EQUAL (EQP X Y) (EQUAL (FIX X) (FIX Y))) (EQUAL (GREATERP X Y) (LESSP Y X)) (EQUAL (LESSEQP X Y) (NOT (LESSP Y X))) (EQUAL (GREATEREQP X Y) (NOT (LESSP X Y))) (EQUAL (BOOLEAN X) (OR (EQUAL X (T)) (EQUAL X (F)))) (EQUAL (IFF X Y) (AND (IMPLIES X Y) (IMPLIES Y X))) (EQUAL (EVEN1 X) (IF (ZEROP X) (T) (ODD (SUB1 X)))) (EQUAL (COUNTPS- L PRED) (COUNTPS-LOOP L PRED (ZERO))) (EQUAL (FACT- I) (FACT-LOOP I 1)) (EQUAL (REVERSE- X) (REVERSE-LOOP X (NIL))) (EQUAL (DIVIDES X Y) (ZEROP (REMAINDER Y X))) (EQUAL (ASSUME-TRUE VAR ALIST) (CONS (CONS VAR (T)) ALIST)) (EQUAL (ASSUME-FALSE VAR ALIST) (CONS (CONS VAR (F)) ALIST)) (EQUAL (TAUTOLOGY-CHECKER X) (TAUTOLOGYP (NORMALIZE X) (NIL))) (EQUAL (FALSIFY X) (FALSIFY1 (NORMALIZE X) (NIL))) (EQUAL (PRIME X) (AND (NOT (ZEROP X)) (NOT (EQUAL X (ADD1 (ZERO)))) (PRIME1 X (SUB1 X)))) (EQUAL (AND P Q) (IF P (IF Q (T) (F)) (F))) (EQUAL (OR P Q) (IF P (T) (IF Q (T) (F)) (F))) (EQUAL (NOT P) (IF P (F) (T))) (EQUAL (IMPLIES P Q) (IF P (IF Q (T) (F)) (T))) (EQUAL (FIX X) (IF (NUMBERP X) X (ZERO))) (EQUAL (IF (IF A B C) D E) (IF A (IF B D E) (IF C D E))) (EQUAL (ZEROP X) (OR (EQUAL X (ZERO)) (NOT (NUMBERP X)))) (EQUAL (PLUS (PLUS X Y) Z) (PLUS X (PLUS Y Z))) (EQUAL (EQUAL (PLUS A B) (ZERO)) (AND (ZEROP A) (ZEROP B))) (EQUAL (DIFFERENCE X X) (ZERO)) (EQUAL (EQUAL (PLUS A B) (PLUS A C)) (EQUAL (FIX B) (FIX C))) (EQUAL (EQUAL (ZERO) (DIFFERENCE X Y)) (NOT (LESSP Y X))) (EQUAL (EQUAL X (DIFFERENCE X Y)) (AND (NUMBERP X) (OR (EQUAL X (ZERO)) (ZEROP Y)))) (EQUAL (MEANING (PLUS-TREE (APPEND X Y)) A) (PLUS (MEANING (PLUS-TREE X) A) (MEANING (PLUS-TREE Y) A))) (EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X)) A) (FIX (MEANING X A))) (EQUAL (APPEND (APPEND X Y) Z) (APPEND X (APPEND Y Z))) (EQUAL (REVERSE (APPEND A B)) (APPEND (REVERSE B) (REVERSE A))) (EQUAL (TIMES X (PLUS Y Z)) (PLUS (TIMES X Y) (TIMES X Z))) (EQUAL (TIMES (TIMES X Y) Z) (TIMES X (TIMES Y Z))) (EQUAL (EQUAL (TIMES X Y) (ZERO)) (OR (ZEROP X) (ZEROP Y))) (EQUAL (EXEC (APPEND X Y) PDS ENVRN) (EXEC Y (EXEC X PDS ENVRN) ENVRN)) (EQUAL (MC-FLATTEN X Y) (APPEND (FLATTEN X) Y)) (EQUAL (MEMBER X (APPEND A B)) (OR (MEMBER X A) (MEMBER X B))) (EQUAL (MEMBER X (REVERSE Y)) (MEMBER X Y)) (EQUAL (LENGTH (REVERSE X)) (LENGTH X)) (EQUAL (MEMBER A (INTERSECT B C)) (AND (MEMBER A B) (MEMBER A C))) (EQUAL (NTH (ZERO) I) (ZERO)) (EQUAL (EXP I (PLUS J K)) (TIMES (EXP I J) (EXP I K))) (EQUAL (EXP I (TIMES J K)) (EXP (EXP I J) K)) (EQUAL (REVERSE-LOOP X Y) (APPEND (REVERSE X) Y)) (EQUAL (REVERSE-LOOP X (NIL)) (REVERSE X)) (EQUAL (COUNT-LIST Z (SORT-LP X Y)) (PLUS (COUNT-LIST Z X) (COUNT-LIST Z Y))) (EQUAL (EQUAL (APPEND A B) (APPEND A C)) (EQUAL B C)) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) (FIX X)) (EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE) BASE) (PLUS (POWER-EVAL L BASE) I)) (EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE) BASE) (PLUS I (PLUS (POWER-EVAL X BASE) (POWER-EVAL Y BASE)))) (EQUAL (REMAINDER Y 1) (ZERO)) (EQUAL (LESSP (REMAINDER X Y) Y) (NOT (ZEROP Y))) (EQUAL (REMAINDER X X) (ZERO)) (EQUAL (LESSP (QUOTIENT I J) I) (AND (NOT (ZEROP I)) (OR (ZEROP J) (NOT (EQUAL J 1))))) (EQUAL (LESSP (REMAINDER X Y) X) (AND (NOT (ZEROP Y)) (NOT (ZEROP X)) (NOT (LESSP X Y)))) (EQUAL (POWER-EVAL (POWER-REP I BASE) BASE) (FIX I)) (EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE) (POWER-REP J BASE) (ZERO) BASE) BASE) (PLUS I J)) (EQUAL (GCD X Y) (GCD Y X)) (EQUAL (NTH (APPEND A B) I) (APPEND (NTH A I) (NTH B (DIFFERENCE I (LENGTH A))))) (EQUAL (DIFFERENCE (PLUS X Y) X) (FIX Y)) (EQUAL (DIFFERENCE (PLUS Y X) X) (FIX Y)) (EQUAL (DIFFERENCE (PLUS X Y) (PLUS X Z)) (DIFFERENCE Y Z)) (EQUAL (TIMES X (DIFFERENCE C W)) (DIFFERENCE (TIMES C X) (TIMES W X))) (EQUAL (REMAINDER (TIMES X Z) Z) (ZERO)) (EQUAL (DIFFERENCE (PLUS B (PLUS A C)) A) (PLUS B C)) (EQUAL (DIFFERENCE (ADD1 (PLUS Y Z)) Z) (ADD1 Y)) (EQUAL (LESSP (PLUS X Y) (PLUS X Z)) (LESSP Y Z)) (EQUAL (LESSP (TIMES X Z) (TIMES Y Z)) (AND (NOT (ZEROP Z)) (LESSP X Y))) (EQUAL (LESSP Y (PLUS X Y)) (NOT (ZEROP X))) (EQUAL (GCD (TIMES X Z) (TIMES Y Z)) (TIMES Z (GCD X Y))) (EQUAL (VALUE (NORMALIZE X) A) (VALUE X A)) (EQUAL (EQUAL (FLATTEN X) (CONS Y (NIL))) (AND (NLISTP X) (EQUAL X Y))) (EQUAL (LISTP (GOPHER X)) (LISTP X)) (EQUAL (SAMEFRINGE X Y) (EQUAL (FLATTEN X) (FLATTEN Y))) (EQUAL (EQUAL (GREATEST-FACTOR X Y) (ZERO)) (AND (OR (ZEROP Y) (EQUAL Y 1)) (EQUAL X (ZERO)))) (EQUAL (EQUAL (GREATEST-FACTOR X Y) 1) (EQUAL X 1)) (EQUAL (NUMBERP (GREATEST-FACTOR X Y)) (NOT (AND (OR (ZEROP Y) (EQUAL Y 1)) (NOT (NUMBERP X))))) (EQUAL (TIMES-LIST (APPEND X Y)) (TIMES (TIMES-LIST X) (TIMES-LIST Y))) (EQUAL (PRIME-LIST (APPEND X Y)) (AND (PRIME-LIST X) (PRIME-LIST Y))) (EQUAL (EQUAL Z (TIMES W Z)) (AND (NUMBERP Z) (OR (EQUAL Z (ZERO)) (EQUAL W 1)))) (EQUAL (GREATEREQPR X Y) (NOT (LESSP X Y))) (EQUAL (EQUAL X (TIMES X Y)) (OR (EQUAL X (ZERO)) (AND (NUMBERP X) (EQUAL Y 1)))) (EQUAL (REMAINDER (TIMES Y X) Y) (ZERO)) (EQUAL (EQUAL (TIMES A B) 1) (AND (NOT (EQUAL A (ZERO))) (NOT (EQUAL B (ZERO))) (NUMBERP A) (NUMBERP B) (EQUAL (SUB1 A) (ZERO)) (EQUAL (SUB1 B) (ZERO)))) (EQUAL (LESSP (LENGTH (DELETE X L)) (LENGTH L)) (MEMBER X L)) (EQUAL (SORT2 (DELETE X L)) (DELETE X (SORT2 L))) (EQUAL (DSORT X) (SORT2 X)) (EQUAL (LENGTH (CONS X1 (CONS X2 (CONS X3 (CONS X4 (CONS X5 (CONS X6 X7))))))) (PLUS 6 (LENGTH X7))) (EQUAL (DIFFERENCE (ADD1 (ADD1 X)) 2) (FIX X)) (EQUAL (QUOTIENT (PLUS X (PLUS X Y)) 2) (PLUS X (QUOTIENT Y 2))) (EQUAL (SIGMA (ZERO) I) (QUOTIENT (TIMES I (ADD1 I)) 2)) (EQUAL (PLUS X (ADD1 Y)) (IF (NUMBERP Y) (ADD1 (PLUS X Y)) (ADD1 X))) (EQUAL (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y)) (IF (LESSP X Y) (NOT (LESSP Y Z)) (IF (LESSP Z Y) (NOT (LESSP Y X)) (EQUAL (FIX X) (FIX Z))))) (EQUAL (MEANING (PLUS-TREE (DELETE X Y)) A) (IF (MEMBER X Y) (DIFFERENCE (MEANING (PLUS-TREE Y) A) (MEANING X A)) (MEANING (PLUS-TREE Y) A))) (EQUAL (TIMES X (ADD1 Y)) (IF (NUMBERP Y) (PLUS X (TIMES X Y)) (FIX X))) (EQUAL (NTH (NIL) I) (IF (ZEROP I) (NIL) (ZERO))) (EQUAL (LAST (APPEND A B)) (IF (LISTP B) (LAST B) (IF (LISTP A) (CONS (CAR (LAST A)) B) B))) (EQUAL (EQUAL (LESSP X Y) Z) (IF (LESSP X Y) (EQUAL T Z) (EQUAL F Z))) (EQUAL (ASSIGNMENT X (APPEND A B)) (IF (ASSIGNEDP X A) (ASSIGNMENT X A) (ASSIGNMENT X B))) (EQUAL (CAR (GOPHER X)) (IF (LISTP X) (CAR (FLATTEN X)) (ZERO))) (EQUAL (FLATTEN (CDR (GOPHER X))) (IF (LISTP X) (CDR (FLATTEN X)) (CONS (ZERO) (NIL)))) (EQUAL (QUOTIENT (TIMES Y X) Y) (IF (ZEROP Y) (ZERO) (FIX X))) (EQUAL (GET J (SET I VAL MEM)) (IF (EQP J I) VAL (GET J MEM)))))))) (TAUTOLOGYP (LAMBDA (X TRUE-LST FALSE-LST) (COND ((TRUEP X TRUE-LST) T) ((FALSEP X FALSE-LST) NIL) ((NLISTP X) NIL) ((EQ (CAR X) (QUOTE IF)) (COND ((TRUEP (CADR X) TRUE-LST) (TAUTOLOGYP (CADDR X) TRUE-LST FALSE-LST)) ((FALSEP (CADR X) FALSE-LST) (TAUTOLOGYP (CADDDR X) TRUE-LST FALSE-LST)) (T (AND (TAUTOLOGYP (CADDR X) (CONS (CADR X) TRUE-LST) FALSE-LST) (TAUTOLOGYP (CADDDR X) TRUE-LST (CONS (CADR X) FALSE-LST)))))) (T NIL)))) (TAUTP (LAMBDA (X) (TAUTOLOGYP (REWRITE X) NIL NIL))) (TEST (LAMBDA NIL (PROG (TM1 TM2 ANS TERM) (SETQ TM1 (PTIME)) (SETQ TERM (APPLY-SUBST (QUOTE ((X F (PLUS (PLUS A B) (PLUS C (ZERO)))) (Y F (TIMES (TIMES A B) (PLUS C D))) (Z F (REVERSE (APPEND (APPEND A B) (NIL)))) (U EQUAL (PLUS A B) (DIFFERENCE X Y)) (W LESSP (REMAINDER A B) (MEMBER A (LENGTH B))))) (QUOTE (IMPLIES (AND (IMPLIES X Y) (AND (IMPLIES Y Z) (AND (IMPLIES Z U) (IMPLIES U W)))) (IMPLIES X W))))) (SETQ ANS (TAUTP TERM)) (SETQ TM2 (PTIME)) (RETURN (LIST ANS (DIFFERENCE (CAR TM2) (CAR TM1)) (DIFFERENCE (CDR TM2) (CDR TM1))))))) (TRANS-OF-IMPLIES (LAMBDA (N) (LIST (QUOTE IMPLIES) (TRANS-OF-IMPLIES1 N) (LIST (QUOTE IMPLIES) 0 N)))) (TRANS-OF-IMPLIES1 (LAMBDA (N) (COND ((EQUAL N 1) (LIST (QUOTE IMPLIES) 0 1)) (T (LIST (QUOTE AND) (LIST (QUOTE IMPLIES) (SUB1 N) N) (TRANS-OF-IMPLIES1 (SUB1 N))))))) (TRUEP (LAMBDA (X LST) (OR (EQUAL X (QUOTE (T))) (MEMBER X LST)))) ) (PUTPROPS MEMBER BLKLIBRARYDEF (LAMBDA (.BLKVAR.X .BLKVAR.Y) (DECLARE (LOCALVARS . T)) (PROG NIL LP (RETURN (COND ((NLISTP .BLKVAR.Y) NIL) ((EQUAL .BLKVAR.X (CAR .BLKVAR.Y) ) .BLKVAR.Y) (T (SETQ .BLKVAR.Y (CDR .BLKVAR.Y)) (GO LP))))))) [DECLARE: DONTEVAL@LOAD DOEVAL@COMPILE DONTCOPY (BLOCK: REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES TEST SETUP) (BLKLIBRARY EQUAL MEMBER GETPROP) (GLOBALVARS TEMP-TEMP UNIFY-SUBST)) ] (DECLARE: DONTCOPY (FILEMAP (NIL (1018 14165 (ADD-LEMMA 1030 . 1573) (ADD-LEMMA-LST 1577 . 1708) (APPLY-SUBST 1712 . 1945) (APPLY-SUBST-LST 1949 . 2119) (FALSEP 2123 . 2200) (ONE-WAY-UNIFY 2204 . 2315) (ONE-WAY-UNIFY1 2319 . 2717) ( ONE-WAY-UNIFY1-LST 2721 . 2928) (PTIME 2932 . 3077) (REWRITE 3081 . 3295 ) (REWRITE-ARGS 3299 . 3441) (REWRITE-WITH-LEMMAS 3445 . 3679) (SETUP 3683 . 12295) (TAUTOLOGYP 12299 . 12890) (TAUTP 12894 . 12958) (TEST 12962 . 13720) (TRANS-OF-IMPLIES 13724 . 13846) (TRANS-OF-IMPLIES1 13850 . 14082) (TRUEP 14086 . 14162))))) STOP The Maclisp Code (DECLARE (SPECIAL UNIFY-SUBST TEMP-TEMP)) (DEFUN PTIME NIL (LIST (RUNTIME) (STATUS GCTIME))) (DEFUN ADD-LEMMA (TERM) (COND ((AND (NOT (ATOM TERM)) (EQ (CAR TERM) (QUOTE EQUAL)) (NOT (ATOM (CADR TERM)))) (PUTPROP (CAR (CADR TERM)) (CONS TERM (GET (CAR (CADR TERM)) (QUOTE LEMMAS))) (QUOTE LEMMAS))) (T (ERROR (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM) TERM)))) (DEFUN ADD-LEMMA-LST (LST) (COND ((NULL LST) T) (T (ADD-LEMMA (CAR LST)) (ADD-LEMMA-LST (CDR LST))))) (DEFUN APPLY-SUBST (ALIST TERM) (COND ((ATOM TERM) (COND ((SETQ TEMP-TEMP (ASSQ TERM ALIST)) (CDR TEMP-TEMP)) (T TERM))) (T (CONS (CAR TERM) (APPLY-SUBST-LST ALIST (CDR TERM)))))) (DEFUN APPLY-SUBST-LST (ALIST LST) (COND ((NULL LST) NIL) (T (CONS (APPLY-SUBST ALIST (CAR LST)) (APPLY-SUBST-LST ALIST (CDR LST)))))) (DEFUN FALSEP (X LST) (OR (EQUAL X (QUOTE (F))) (MEMBER X LST))) (DEFUN ONE-WAY-UNIFY (TERM1 TERM2) (PROGN (SETQ UNIFY-SUBST NIL) (ONE-WAY-UNIFY1 TERM1 TERM2))) (DEFUN ONE-WAY-UNIFY1 (TERM1 TERM2) (COND ((ATOM TERM2) (COND ((SETQ TEMP-TEMP (ASSQ TERM2 UNIFY-SUBST)) (EQUAL TERM1 (CDR TEMP-TEMP))) (T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1) UNIFY-SUBST)) T))) ((ATOM TERM1) NIL) ((EQ (CAR TERM1) (CAR TERM2)) (ONE-WAY-UNIFY1-LST (CDR TERM1) (CDR TERM2))) (T NIL))) (DEFUN ONE-WAY-UNIFY1-LST (LST1 LST2) (COND ((NULL LST1) T) ((ONE-WAY-UNIFY1 (CAR LST1) (CAR LST2)) (ONE-WAY-UNIFY1-LST (CDR LST1) (CDR LST2))) (T NIL))) (DEFUN REWRITE (TERM) (COND ((ATOM TERM) TERM) (T (REWRITE-WITH-LEMMAS (CONS (CAR TERM) (REWRITE-ARGS (CDR TERM))) (GET (CAR TERM) (QUOTE LEMMAS)))))) (DEFUN REWRITE-ARGS (LST) (COND ((NULL LST) NIL) (T (CONS (REWRITE (CAR LST)) (REWRITE-ARGS (CDR LST)))))) (DEFUN REWRITE-WITH-LEMMAS (TERM LST) (COND ((NULL LST) TERM) ((ONE-WAY-UNIFY TERM (CADR (CAR LST))) (REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST))))) (T (REWRITE-WITH-LEMMAS TERM (CDR LST))))) (DEFUN SETUP NIL (ADD-LEMMA-LST (QUOTE ((EQUAL (COMPILE FORM) (REVERSE (CODEGEN (OPTIMIZE FORM) (NIL)))) (EQUAL (EQP X Y) (EQUAL (FIX X) (FIX Y))) (EQUAL (GREATERP X Y) (LESSP Y X)) (EQUAL (LESSEQP X Y) (NOT (LESSP Y X))) (EQUAL (GREATEREQP X Y) (NOT (LESSP X Y))) (EQUAL (BOOLEAN X) (OR (EQUAL X (T)) (EQUAL X (F)))) (EQUAL (IFF X Y) (AND (IMPLIES X Y) (IMPLIES Y X))) (EQUAL (EVEN1 X) (IF (ZEROP X) (T) (ODD (SUB1 X)))) (EQUAL (COUNTPS- L PRED) (COUNTPS-LOOP L PRED (ZERO))) (EQUAL (FACT- I) (FACT-LOOP I 1)) (EQUAL (REVERSE- X) (REVERSE-LOOP X (NIL))) (EQUAL (DIVIDES X Y) (ZEROP (REMAINDER Y X))) (EQUAL (ASSUME-TRUE VAR ALIST) (CONS (CONS VAR (T)) ALIST)) (EQUAL (ASSUME-FALSE VAR ALIST) (CONS (CONS VAR (F)) ALIST)) (EQUAL (TAUTOLOGY-CHECKER X) (TAUTOLOGYP (NORMALIZE X) (NIL))) (EQUAL (FALSIFY X) (FALSIFY1 (NORMALIZE X) (NIL))) (EQUAL (PRIME X) (AND (NOT (ZEROP X)) (NOT (EQUAL X (ADD1 (ZERO)))) (PRIME1 X (SUB1 X)))) (EQUAL (AND P Q) (IF P (IF Q (T) (F)) (F))) (EQUAL (OR P Q) (IF P (T) (IF Q (T) (F)) (F))) (EQUAL (NOT P) (IF P (F) (T))) (EQUAL (IMPLIES P Q) (IF P (IF Q (T) (F)) (T))) (EQUAL (FIX X) (IF (NUMBERP X) X (ZERO))) (EQUAL (IF (IF A B C) D E) (IF A (IF B D E) (IF C D E))) (EQUAL (ZEROP X) (OR (EQUAL X (ZERO)) (NOT (NUMBERP X)))) (EQUAL (PLUS (PLUS X Y) Z) (PLUS X (PLUS Y Z))) (EQUAL (EQUAL (PLUS A B) (ZERO)) (AND (ZEROP A) (ZEROP B))) (EQUAL (DIFFERENCE X X) (ZERO)) (EQUAL (EQUAL (PLUS A B) (PLUS A C)) (EQUAL (FIX B) (FIX C))) (EQUAL (EQUAL (ZERO) (DIFFERENCE X Y)) (NOT (LESSP Y X))) (EQUAL (EQUAL X (DIFFERENCE X Y)) (AND (NUMBERP X) (OR (EQUAL X (ZERO)) (ZEROP Y)))) (EQUAL (MEANING (PLUS-TREE (APPEND X Y)) A) (PLUS (MEANING (PLUS-TREE X) A) (MEANING (PLUS-TREE Y) A))) (EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X)) A) (FIX (MEANING X A))) (EQUAL (APPEND (APPEND X Y) Z) (APPEND X (APPEND Y Z))) (EQUAL (REVERSE (APPEND A B)) (APPEND (REVERSE B) (REVERSE A))) (EQUAL (TIMES X (PLUS Y Z)) (PLUS (TIMES X Y) (TIMES X Z))) (EQUAL (TIMES (TIMES X Y) Z) (TIMES X (TIMES Y Z))) (EQUAL (EQUAL (TIMES X Y) (ZERO)) (OR (ZEROP X) (ZEROP Y))) (EQUAL (EXEC (APPEND X Y) PDS ENVRN) (EXEC Y (EXEC X PDS ENVRN) ENVRN)) (EQUAL (MC-FLATTEN X Y) (APPEND (FLATTEN X) Y)) (EQUAL (MEMBER X (APPEND A B)) (OR (MEMBER X A) (MEMBER X B))) (EQUAL (MEMBER X (REVERSE Y)) (MEMBER X Y)) (EQUAL (LENGTH (REVERSE X)) (LENGTH X)) (EQUAL (MEMBER A (INTERSECT B C)) (AND (MEMBER A B) (MEMBER A C))) (EQUAL (NTH (ZERO) I) (ZERO)) (EQUAL (EXP I (PLUS J K)) (TIMES (EXP I J) (EXP I K))) (EQUAL (EXP I (TIMES J K)) (EXP (EXP I J) K)) (EQUAL (REVERSE-LOOP X Y) (APPEND (REVERSE X) Y)) (EQUAL (REVERSE-LOOP X (NIL)) (REVERSE X)) (EQUAL (COUNT-LIST Z (SORT-LP X Y)) (PLUS (COUNT-LIST Z X) (COUNT-LIST Z Y))) (EQUAL (EQUAL (APPEND A B) (APPEND A C)) (EQUAL B C)) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) (FIX X)) (EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE) BASE) (PLUS (POWER-EVAL L BASE) I)) (EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE) BASE) (PLUS I (PLUS (POWER-EVAL X BASE) (POWER-EVAL Y BASE)))) (EQUAL (REMAINDER Y 1) (ZERO)) (EQUAL (LESSP (REMAINDER X Y) Y) (NOT (ZEROP Y))) (EQUAL (REMAINDER X X) (ZERO)) (EQUAL (LESSP (QUOTIENT I J) I) (AND (NOT (ZEROP I)) (OR (ZEROP J) (NOT (EQUAL J 1))))) (EQUAL (LESSP (REMAINDER X Y) X) (AND (NOT (ZEROP Y)) (NOT (ZEROP X)) (NOT (LESSP X Y)))) (EQUAL (POWER-EVAL (POWER-REP I BASE) BASE) (FIX I)) (EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE) (POWER-REP J BASE) (ZERO) BASE) BASE) (PLUS I J)) (EQUAL (GCD X Y) (GCD Y X)) (EQUAL (NTH (APPEND A B) I) (APPEND (NTH A I) (NTH B (DIFFERENCE I (LENGTH A))))) (EQUAL (DIFFERENCE (PLUS X Y) X) (FIX Y)) (EQUAL (DIFFERENCE (PLUS Y X) X) (FIX Y)) (EQUAL (DIFFERENCE (PLUS X Y) (PLUS X Z)) (DIFFERENCE Y Z)) (EQUAL (TIMES X (DIFFERENCE C W)) (DIFFERENCE (TIMES C X) (TIMES W X))) (EQUAL (REMAINDER (TIMES X Z) Z) (ZERO)) (EQUAL (DIFFERENCE (PLUS B (PLUS A C)) A) (PLUS B C)) (EQUAL (DIFFERENCE (ADD1 (PLUS Y Z)) Z) (ADD1 Y)) (EQUAL (LESSP (PLUS X Y) (PLUS X Z)) (LESSP Y Z)) (EQUAL (LESSP (TIMES X Z) (TIMES Y Z)) (AND (NOT (ZEROP Z)) (LESSP X Y))) (EQUAL (LESSP Y (PLUS X Y)) (NOT (ZEROP X))) (EQUAL (GCD (TIMES X Z) (TIMES Y Z)) (TIMES Z (GCD X Y))) (EQUAL (VALUE (NORMALIZE X) A) (VALUE X A)) (EQUAL (EQUAL (FLATTEN X) (CONS Y (NIL))) (AND (NLISTP X) (EQUAL X Y))) (EQUAL (LISTP (GOPHER X)) (LISTP X)) (EQUAL (SAMEFRINGE X Y) (EQUAL (FLATTEN X) (FLATTEN Y))) (EQUAL (EQUAL (GREATEST-FACTOR X Y) (ZERO)) (AND (OR (ZEROP Y) (EQUAL Y 1)) (EQUAL X (ZERO)))) (EQUAL (EQUAL (GREATEST-FACTOR X Y) 1) (EQUAL X 1)) (EQUAL (NUMBERP (GREATEST-FACTOR X Y)) (NOT (AND (OR (ZEROP Y) (EQUAL Y 1)) (NOT (NUMBERP X))))) (EQUAL (TIMES-LIST (APPEND X Y)) (TIMES (TIMES-LIST X) (TIMES-LIST Y))) (EQUAL (PRIME-LIST (APPEND X Y)) (AND (PRIME-LIST X) (PRIME-LIST Y))) (EQUAL (EQUAL Z (TIMES W Z)) (AND (NUMBERP Z) (OR (EQUAL Z (ZERO)) (EQUAL W 1)))) (EQUAL (GREATEREQPR X Y) (NOT (LESSP X Y))) (EQUAL (EQUAL X (TIMES X Y)) (OR (EQUAL X (ZERO)) (AND (NUMBERP X) (EQUAL Y 1)))) (EQUAL (REMAINDER (TIMES Y X) Y) (ZERO)) (EQUAL (EQUAL (TIMES A B) 1) (AND (NOT (EQUAL A (ZERO))) (NOT (EQUAL B (ZERO))) (NUMBERP A) (NUMBERP B) (EQUAL (SUB1 A) (ZERO)) (EQUAL (SUB1 B) (ZERO)))) (EQUAL (LESSP (LENGTH (DELETE X L)) (LENGTH L)) (MEMBER X L)) (EQUAL (SORT2 (DELETE X L)) (DELETE X (SORT2 L))) (EQUAL (DSORT X) (SORT2 X)) (EQUAL (LENGTH (CONS X1 (CONS X2 (CONS X3 (CONS X4 (CONS X5 (CONS X6 X7))))))) (PLUS 6 (LENGTH X7))) (EQUAL (DIFFERENCE (ADD1 (ADD1 X)) 2) (FIX X)) (EQUAL (QUOTIENT (PLUS X (PLUS X Y)) 2) (PLUS X (QUOTIENT Y 2))) (EQUAL (SIGMA (ZERO) I) (QUOTIENT (TIMES I (ADD1 I)) 2)) (EQUAL (PLUS X (ADD1 Y)) (IF (NUMBERP Y) (ADD1 (PLUS X Y)) (ADD1 X))) (EQUAL (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y)) (IF (LESSP X Y) (NOT (LESSP Y Z)) (IF (LESSP Z Y) (NOT (LESSP Y X)) (EQUAL (FIX X) (FIX Z))))) (EQUAL (MEANING (PLUS-TREE (DELETE X Y)) A) (IF (MEMBER X Y) (DIFFERENCE (MEANING (PLUS-TREE Y) A) (MEANING X A)) (MEANING (PLUS-TREE Y) A))) (EQUAL (TIMES X (ADD1 Y)) (IF (NUMBERP Y) (PLUS X (TIMES X Y)) (FIX X))) (EQUAL (NTH (NIL) I) (IF (ZEROP I) (NIL) (ZERO))) (EQUAL (LAST (APPEND A B)) (IF (LISTP B) (LAST B) (IF (LISTP A) (CONS (CAR (LAST A)) B) B))) (EQUAL (EQUAL (LESSP X Y) Z) (IF (LESSP X Y) (EQUAL T Z) (EQUAL F Z))) (EQUAL (ASSIGNMENT X (APPEND A B)) (IF (ASSIGNEDP X A) (ASSIGNMENT X A) (ASSIGNMENT X B))) (EQUAL (CAR (GOPHER X)) (IF (LISTP X) (CAR (FLATTEN X)) (ZERO))) (EQUAL (FLATTEN (CDR (GOPHER X))) (IF (LISTP X) (CDR (FLATTEN X)) (CONS (ZERO) (NIL)))) (EQUAL (QUOTIENT (TIMES Y X) Y) (IF (ZEROP Y) (ZERO) (FIX X))) (EQUAL (GET J (SET I VAL MEM)) (IF (EQP J I) VAL (GET J MEM))))))) (DEFUN TAUTOLOGYP (X TRUE-LST FALSE-LST) (COND ((TRUEP X TRUE-LST) T) ((FALSEP X FALSE-LST) NIL) ((ATOM X) NIL) ((EQ (CAR X) (QUOTE IF)) (COND ((TRUEP (CADR X) TRUE-LST) (TAUTOLOGYP (CADDR X) TRUE-LST FALSE-LST)) ((FALSEP (CADR X) FALSE-LST) (TAUTOLOGYP (CADDDR X) TRUE-LST FALSE-LST)) (T (AND (TAUTOLOGYP (CADDR X) (CONS (CADR X) TRUE-LST) FALSE-LST) (TAUTOLOGYP (CADDDR X) TRUE-LST (CONS (CADR X) FALSE-LST)))))) (T NIL))) (DEFUN TAUTP (X) (TAUTOLOGYP (REWRITE X) NIL NIL)) (DEFUN TEST NIL (PROG (TM1 TM2 ANS TERM) (SETQ TM1 (PTIME)) (SETQ TERM (APPLY-SUBST (QUOTE ((X F (PLUS (PLUS A B) (PLUS C (ZERO)))) (Y F (TIMES (TIMES A B) (PLUS C D))) (Z F (REVERSE (APPEND (APPEND A B) (NIL)))) (U EQUAL (PLUS A B) (DIFFERENCE X Y)) (W LESSP (REMAINDER A B) (MEMBER A (LENGTH B))))) (QUOTE (IMPLIES (AND (IMPLIES X Y) (AND (IMPLIES Y Z) (AND (IMPLIES Z U) (IMPLIES U W)))) (IMPLIES X W))))) (SETQ ANS (TAUTP TERM)) (SETQ TM2 (PTIME)) (RETURN (LIST ANS (DIFFERENCE (CAR TM2) (CAR TM1)) (DIFFERENCE (CADR TM2) (CADR TM1)))))) (DEFUN TRANS-OF-IMPLIES (N) (LIST (QUOTE IMPLIES) (TRANS-OF-IMPLIES1 N) (LIST (QUOTE IMPLIES) 0 N))) (DEFUN TRANS-OF-IMPLIES1 (N) (COND ((EQUAL N 1) (LIST (QUOTE IMPLIES) 0 1)) (T (LIST (QUOTE AND) (LIST (QUOTE IMPLIES) (SUB1 N) N) (TRANS-OF-IMPLIES1 (SUB1 N)))))) (DEFUN TRUEP (X LST) (OR (EQUAL X (QUOTE (T))) (MEMBER X LST))) The ELISP test [PHOTO: Recording initiated Tue 29-Jun-82 12:23PM] LINK FROM CL.BOYER, TTY 17 Tops-20 Command Processor 4A(67)-1 End of <CL.BOYER>COMAND.CMD.1 @<ELISP>ELISP [Keeping] Elisp, 4 27 82 *(DSKIN "EREWRITE.FLAP") "EREWRITE.FLAP.2" Files-Loaded *(SETUP) T *(TEST) 19776 msec CPU (7447 msec GC), 41583 msec clock, 452930 words consed (T) *(TEST) 18185 msec CPU (6361 msec GC), 51621 msec clock, 452930 words consed (T) *↑C @POP [PHOTO: Recording terminated Tue 29-Jun-82 12:26PM] Interlisp bcompl blocklib swap and noswap [PHOTO: Recording initiated Mon 5-Jul-82 12:16PM] LINK FROM CL.BOYER, TTY 17 Tops-20 Command Processor 4B(70)-1 End of <CL.BOYER>COMAND.CMD.1 @LISP.EXE.133 INTERLISP-10 27-NOV-79 ... collecting lists 716, 10444 free cells control-A is an interrupt and can't be an edit control-character Good afternoon, Bob. 2←LOAD(IREWRITE.COM] compiled on 5-Jul-82 12:11:29 FILE CREATED 5-Jul-82 12:11:22 IREWRITECOMS <CL.BOYER.LISPS>IREWRITE.COM.3 3←IREWRITECOMS ((FNS * IREWRITEFNS) (PROP BLKLIBRARYDEF MEMBER SASSOC) (BLOCKS (REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES TEST SETUP) (BLKLIBRARY EQUAL MEMBER GETPROP) (GLOBALVARS TEMP-TEMP UNIFY-SUBST) ))) 4←NOSWAPFLG NIL 5←(MINFS 100000] 10000 6←(RECLAIM] collecting lists 7245, 92749 free cells, 0 pages left 92749 7←(GCGAG] 40 8←(MINFS 10000] 100000 9←SETUP] T 10←(TEST] (T 15821 4995) 11←(TEST] (T 17498 6245) 12←(TEST] (T 16569 5954) 13←(TEST] (T 16707 5925) 14←(SETQ NOSWAPFLG T] (NOSWAPFLG reset) T 15←LOAD(IREWRITE.COM] compiled on 5-Jul-82 12:11:29 FILE CREATED 5-Jul-82 12:11:22 (REWRITEBLOCK redefined) (TEST redefined) (SETUP redefined) IREWRITECOMS <CL.BOYER.LISPS>IREWRITE.COM.3 16←TEST] (T 19546 8561) 17←TEST] (T 17431 6601) 18←TEST] (T 17192 6511) 19←TEST] (T 18785 8161) 20←↑C @POP [PHOTO: Recording terminated Mon 5-Jul-82 12:29PM] Interlisp bcompl no blocklib swap and noswap [PHOTO: Recording initiated Mon 5-Jul-82 12:29PM] LINK FROM CL.BOYER, TTY 17 Tops-20 Command Processor 4B(70)-1 End of <CL.BOYER>COMAND.CMD.1 @LISP.EXE.133 INTERLISP-10 27-NOV-79 ... collecting lists 716, 10444 free cells control-A is an interrupt and can't be an edit control-character Hello, Bob. 2←LOAD(IREWRITE] FILE CREATED 5-Jul-82 12:11:22 IREWRITECOMS <CL.BOYER.LISPS>IREWRITE..3 3←IREWRITECOMS ((FNS * IREWRITEFNS) (PROP BLKLIBRARYDEF MEMBER SASSOC) (BLOCKS (REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES TEST SETUP) (BLKLIBRARY EQUAL MEMBER GETPROP) (GLOBALVARS TEMP-TEMP UNIFY-SUBST) ))) 4←(BLOCKCOMPILE 'REWRITEBLOCK IREWRITEFNS '(TEST SETUP] listing? STore and redefine output file? No (REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP) (REWRITEBLOCK (REWRITEBLOCK#0) (TEMP-TEMP UNIFY-SUBST)) collecting lists 6001, 10097 free cells (TEST NIL NIL) (TEST redefined) (SETUP NIL NIL) (SETUP redefined) (TEST SETUP) 5←(SETUP] T 6←(MINFS 100000] 10000 7←(RECLAIM] collecting lists 9850, 90234 free cells, 0 pages left 90234 8←(MINFS 10000] 100000 9←(GCGAG] 40 10←NOSWAPFLG NIL 11←(TEST] (T 31978 6737) 12←(TEST] (T 47072 6180) 13←(TEST] LISP Running at 30547 Used 0:10:10.7 in 2:40:39, Load 3.06 (T 71046 6316) 14←(TEST] LISP Running at 30525 Used 0:11:45.7 in 2:44:33, Load 2.85 (T 71222 7772) 15←(TEST] (T 70026 6175) 16←(SETQ NOSWAPFLG T] (NOSWAPFLG reset) T 17←REDO BLOCKCOMPILE listing? ST output file? N (REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP) (REWRITEBLOCK (REWRITEBLOCK#0) (TEMP-TEMP UNIFY-SUBST)) (REWRITEBLOCK redefined) (TEST NIL NIL) (TEST redefined) (SETUP NIL NIL) (SETUP redefined) (TEST SETUP) 18←(TEST] (T 46501 7685) 19←TEST] (T 45285 6068) 20←TEST] (T 46995 7564) 21←TEST] (T 46522 6180) 22←↑C @POP [PHOTO: Recording terminated Mon 5-Jul-82 12:51PM] Maclisp [PHOTO: Recording initiated Tue 29-Jun-82 12:26PM] LINK FROM CL.BOYER, TTY 17 Tops-20 Command Processor 4A(67)-1 End of <CL.BOYER>COMAND.CMD.1 @<ATP.MURRAY>MACLSP LISP 1983 Alloc? Y # REGPDL = 4000 # SPECPDL = 2000 # FXPDL = 4000 # FLPDL = 1000 LIST = 40000 100000. SYMBOL = 6000 $ * (SETQ BASE (SETQ IBASE 10.)) 10. (FASLOAD MREWRITE) 40307. (SETUP) T (TEST) (T 20190000. 11905000.) (TEST) (T 13728000. 5236000.) (TEST) (T 13708000. 5398000.) ↑C @POP [PHOTO: Recording terminated Tue 29-Jun-82 12:29PM] ********************************************************************** UCILISP [PHOTO: Recording initiated Wed 30-Jun-82 12:16PM] LINK FROM CL.BOYER, TTY 17 Tops-20 Command Processor 4B(70)-1 End of <CL.BOYER>COMAND.CMD.1 @ @ucilsp UT/UCI LISP - 8/10/80 *(gcgag t) NIL *(gc) 3790 FREE STG, 1129 FULL WORDS AVAILABLE NIL *(expfs 100000.) FREE STG EXHAUSTED FULL WORD SPACE EXHAUSTED 101112 FREE STG, 1131 FULL WORDS AVAILABLE *(loa≠≠≠≠Jdskin (rewrit.lap)) (ADD-LEMMA 32) (ADD-LEMMA-LST 10) (APPLY-SUBST 23) (APPLY-SUBST-LST 15) (FALSEP 10) (ONE-WAY-UNIFY 2) Binary Program Space exceeded *(expbps 1000) FREE STG EXHAUSTED FULL WORD SPACE EXHAUSTED 101012 FREE STG, 1091 FULL WORDS AVAILABLE *(dskin (rewrit.lap)) (ADD-LEMMA 32) (ADD-LEMMA-LST 10) (APPLY-SUBST 23) (APPLY-SUBST-LST 15) (FALSEP 10) (ONE-WAY-UNIFY 2) (ONE-WAY-UNIFY1 38) (ONE-WAY-UNIFY1-LST 15) (REWRITE 20) (REWRITE-ARGS 11) (REWRITE-WITH-LEMMAS 22) (SETUP 2) (TAUTOLOGYP 66) (TAUTP 4) (TEST 2) (TEST1 8) (TRANS-OF-IMPLIES 13) (TRANS-OF-IMPLIES1 31) (TRUEP 10) FILES-LOADED *(setup) T *(test) FREE STG EXHAUSTED 63969 FREE STG, 943 FULL WORDS AVAILABLE FREE STG EXHAUSTED 47018 FREE STG, 943 FULL WORDS AVAILABLE FREE STG EXHAUSTED 40438 FREE STG, 943 FULL WORDS AVAILABLE 50614 msec CPU (3738 msec GC), 67496 msec clock, 226465 conses (T) *(test) FREE STG EXHAUSTED 94012 FREE STG, 942 FULL WORDS AVAILABLE FREE STG EXHAUSTED 58810 FREE STG, 942 FULL WORDS AVAILABLE FREE STG EXHAUSTED 47089 FREE STG, 942 FULL WORDS AVAILABLE FREE STG EXHAUSTED 35091 FREE STG, 942 FULL WORDS AVAILABLE 51676 msec CPU (4605 msec GC), 72196 msec clock, 226467 conses (T) *(test) FREE STG EXHAUSTED 91609 FREE STG, 942 FULL WORDS AVAILABLE FREE STG EXHAUSTED 57005 FREE STG, 942 FULL WORDS AVAILABLE FREE STG EXHAUSTED 45700 FREE STG, 942 FULL WORDS AVAILABLE FREE STG EXHAUSTED 34252 FREE STG, 942 FULL WORDS AVAILABLE 52328 msec CPU (4809 msec GC), 70687 msec clock, 226467 conses (T) *(nouuo nil) T *(test) FREE STG EXHAUSTED 89843 FREE STG, 942 FULL WORDS AVAILABLE FREE STG EXHAUSTED 56841 FREE STG, 942 FULL WORDS AVAILABLE FREE STG EXHAUSTED 45727 FREE STG, 942 FULL WORDS AVAILABLE FREE STG EXHAUSTED 34117 FREE STG, 942 FULL WORDS AVAILABLE 14099 msec CPU (4711 msec GC), 20077 msec clock, 226467 conses (T) *(test) FREE STG EXHAUSTED 89806 FREE STG, 942 FULL WORDS AVAILABLE FREE STG EXHAUSTED 56830 FREE STG, 942 FULL WORDS AVAILABLE FREE STG EXHAUSTED 45727 FREE STG, 942 FULL WORDS AVAILABLE FREE STG EXHAUSTED 34117 FREE STG, 942 FULL WORDS AVAILABLE 13827 msec CPU (4712 msec GC), 19857 msec clock, 226467 conses (T) * @pop [PHOTO: Recording terminated Wed 30-Jun-82 12:24PM] Interlisp (Dolphin and Dorado) Date: 8 Jul 1982 18:56 PDT From: JonL at PARC-MAXC Reply-To: JonL at PARC-MAXC To: NOVAK at SUMEX-AIM cc: CL.BOYER, Masinter at PARC-MAXC, LispCore↑ at PARC-MAXC Re: The Boyer-Moore-Novak Benchmarkings Gordon, I'll have to apologize for waiting so long to get you the results of the timing comparisons between your machine and the various configurations at PARC. I was "laid-low" last Saturday with either a summer flu, or a severe allergic reaction (hay fever), and couldn't get the results summarized until yesterday. I have six areas that I want to summarize in this note: Translation Inadequacy due to the FreeVars Trip-Up "Ineffable" Factors Tending to make timing runs Un-Reproducible PUP Activity -- Ephemeral as well as Ineffable What the Faster Clock on buys What DISPLAYDOWN buys What you can Expect for Dolphin Speed Increases Soon Briefly, the "FreeVars Trip-Up" and the DISPLAYDOWN account for most of the sluggishness of the timings you made, but also there's one "ineffable" which might be sabotaging you. Below these sections, I've tried to display my data in good scientific fashion; you'll note that I give a "First run" time and a "Mode run" time. What this means is the "First run" must absorb all the "ineffable" costs of swapping in the necessary code and data parts, and of initially-building the List-space pages that will be used and re-used on subsequent runs. Also included are one set of timings from a Dorado, just for comparison. Generally, my comparisons will be of "speed" rather than "time". Thus if one trial takes 40 secs, and another takes 50 secs, then the first one runs 25% faster (the other way of saying it would be that the first one takes 20% less time). The rationale is this: the first one "computes" .025 MegaFrumbles per second, while the second one only computes .020 MegaFrumbles per second; hence the speed of the first one is (.025-.020)/.020 = 25% faster than the speed of the second one. Translation Inadequacy due to the FreeVars Trip-Up Actually, it's just as well that I waited until today to report to you, since the **major factor** in the timings compared so far is the old "FreeVars Trip-Up", and anyway Boyer's latest modification is more appropriate for benchmarking, period. I have quite a few interesting timings to report (and a few remaining mysteries regarding your machine), but indeed the major discrepancy between your timings and mine was that the version of IREWRITE we had at Parc is the one that Larry had "diddled" as per his earlier note. On your machine, I saw a 50% speedup due to better treatment of the free variable TEMP-TEMP. (My runs of your original version of IREWRITE compared with Larry's "diddled" version). On several machines here, I compared Larry's "diddled" version with Boyer's new version, and observed about a 9% speed-up of the latter over the former. Converting TEMP-TEMP from a local variable to a GLOBALVAR should cause a slowdown in the 1% range (a GLOBALVAR usage may take time for a GC-hash-table operation, but a LOCALVAR usage takes time only for pushing/popping the stack) but Boyer changed several other bottlenecks and the speed increases therefrom more than compensated for the loss of the local variable (SASSOC ==> FASSOC, and the placement of important properties at the beginning of the proplist ?) In any case, this benchmark exhibits a factor of two improvement by removing what I'm calling the "FreeVars Trip-Up". This point can't be overstressed: that Interlisp-D is a deep-bound implementation, whereas MacLisp and current Interlisp-10 are shallow- bound (Interlisp-10 was first deep-bound, then later shallow-bound), and that the questionable practice of using free variables for local temporaries costs little when they are shallow-bound, but could cost arbitrarily large when deep-bound. I say, "questionable" since a program with such temporaries is semantically the same regardless of whether they are GLOBAL, SPECIAL, or local; furthermore, the general direction of "structured programming" is to avoid free variables at all costs, and to bind temporaries as syntactically "low" as possible. The *default* declaration for variables in Interlisp is SPECVARS, for consistency with the way the interpreter is written, and thus the default compilation of a free variable will cause a stack scan (slow) rather than a reference to the global value cell (fast). So one does have to take *some* action to override the default case when transporting such a program. A recent Symbolics advertising flyer makes a "comparison" of an Interlisp program running on the Dolphin and on the LM-2. It wasn't so much a comparison between Interlisp-D/Dolphin with ZetaLisp/CADR as a documentation of someone's failure to add the appropriate GLOBALVARS delcarations. I heard (admittedly, hearsay) that the ISI guy whose program was under test made the additional declaration himself, and the Dolphin performance "improved by 67%". [One also wonders how the "comparison" would have fared had the LISPMachine garbage collector been operable; a large percentage of the Dolphin time was spent in GC, which helps keep the working-set small, and also allows you to continue running *after* the benchmark has finished running.] "Ineffable" Factors Tending to make timing runs Un-Reproducible As Larry's note indicated, there is a hidden problem with swap time in the Interlisp-D of today -- an "ineffable" amount of it is being charged to CPU time rather than the reported Swap time. The data below seem to indicate anywhere from 5% to 20% of reported CPU time is really swap time, when there is indeed swapping going on. You're quite right, however, that swapping-time is a small factor in this benchmark; although there consistently seemed to be more of it on your machine than mine (about 8%, depending on method of interpretation of the "ineffable" considerations herein mentioned). That's mystery number 1, since both your machine and mine have the same amount of real memory, namely about 1.15 Megabyte. The proper setting of RECLAIMMIN keeps both our Dolphins from "going over the knee" on this benchmark, although a large setting for my Dolphin caused the CPU time to go up by 50% and the Swap time to go up from essentially 0 to almost 600 seconds. A Dorado, with 2 Megabytes and a faster swapping-disk, didn't "go over the knee" even with the extreme high setting of RECLAIMMIN. During the first run of TEST, additional pages are added to LIST space, and the cost of doing this is difficult to estimate accurately in the current setup. The STATS I ran on the Dorado showed nearly 20% of the total first-run time given to this activity, but this is inflated by the fact that the run had to be terminated abnormally (ran out of DSK space for keeping statistics); this "ineffable" time would concentrate in the early part of the run. But a 5%-10% slowdown due to this facter seems indicated in general (my "educated guess" from mulling over the data). There is a certain oddity about the reference-count GC scheme in that a call to RECLAIM may not necessarily recover all reclaimable space. Without going into the details of this oddity, I merely observed that between TEST runs, it was necessary to do several iterations of (RECLAIM) before the time spent therein settled down to a typical low value [indicating that most if not all reclaimables were in fact reclaimed]. This is why I've indicated a "mode" run -- namely the timings that are most often seen after the initial swap-in, initial swell-up of LIST space, and "cleanness" of the reclaimable space are accounted for. But I must confess, that I hadn't discovered all of these things initially, so there is a little uncertainty about the "mode" timings done on July 2. PUP Activity -- Ephemeral as well as Ineffable Mystery number 2 is why the "diddled" TEST run on your machine has a "mode" of 210 CPU seconds as opposed to about 143 CPU seconds on a comparably-clocked machine here running the current CONBRIO release. (This was my measurement for the "diddled" version -- you reported 278 for the original version and I recorded 299. for the original version -- but the "diddled" version is *exactly* the same file I had at PARC, in the same release of Lisp). It's almost as if you had some large overhead activity going on all the time, such as snarfing up random PUPs and throwing them away. Pup activity could be a highly-variable thing, and could account for large timing differences between say Friday afternoon and Thursday morning. Unfortunately, its also something that is not easily controlled by a user doing timings, since it depends the PUP activity of others users of the same ethernet. Currently, time spent in Interlisp-D "dropping" non- intended PUPs is not visible in the timings statistics (it would merely bloat reported CPU time). PUP activity could be monitored by another Dolphin running EtherWatch while you are running timings on yours. [A simple way of temporarily turning off PUP activity might help filter out this as a source of variability; are you interested in trying?] What the Faster Clock on buys My Dolphin is indeed faster than many others, because it has a clock crystal running at 44.5 MegaHertz. The Dolphin was originally intended to run at 50MHz, but due to a larger-than-expected variability in the components (chips, etc) the production models are currently pegged at 40MHz. Machines with a 44.5MHz clock have a speed increase of about 12% to 16%. The reason why this isn't merely 10% is that there is a "buffering" action of the constant-time overhead required for maintaining the display and sampling the keyboard; thus a faster machine spends proportionately less of its time in these constant overhead tasks. Of course, 50MHz clocks would result in even more performance improvement. What DISPLAYDOWN buys I thought that you had run with DISPLAYDOWN during the compute- bound TEST; so I ran this way on my runs, except for those intended to gather data which would correlate the effect of DISPLAYDOWN. It makes sense to do so on *compute-bound* tasks, since an average speed increase of 41% to 45% is thereby obtained. As expected, the display off means more to CPU time on a 40MHz machine than to that on a 44.5MHz one -- 43% as opposed to only 36%. GC timings are so variable that I factored them out for these percentages. [I don't think one would see anything like this gain if the keyboard sampling mentioned above were similarly shut off; Dorado STATS point to maybe 6% possible, but even this overhead cost may go down as more software is developed. As a side comment, display maintenance is not a significant factor in the Dorado or in the DandeLion.] What you can Expect for Dolphin Speed Increases Soon The WIND version of the software will likely be released later this year, and the data herein indicate a minimum of about 10% overall increase in speed; other preliminary measures suggest a speed-up of 15% to 20%. Faster hardware may be in the works, but I'm not the one to comment in any offical way about this. Maybe when we get some more benchmarks (such as Dick Gabriel is pushing for), we'll do them on the latest Dolphins. Just for the record, I'd like to include some timings given me by Larry, which were done on the Dolphin of one year ago (the "diddled" version of the problem): Swap time = 30secs GC time = 175secs CPU time = 750secs Elapsed = 950secs So today's "vanilla" times are 5.6 times faster than last years, and on my 44.5Mhz machine running WIND I see a speed-up of a factor of 7. A factor of 7! Bill van Melle suggests that these speed-ups are due mainly to improvements in function call and CONS, and that's precisely what the Boyer-Moore IREWRITE benchmark tests. I really don't think anything quite that dramatic is on the horizon for the *overall* Dolphin performance, but *selected areas* which we have targeted for more devolpment could show stellar improvement. (such as putting floating-point into microcode). Hope to see you at AAAI. _________________________________________________ The Raw Data Machines: GSN (Gordon Novak's), JONL (mine), SYBAL (John Sybalsky's) [GSN and SYBAL have 40MHz, JONL has 44.5MHz] Finisterra (the only Dorado included) Program: OB (Old Boyer code, without declarations) NB (New Boyer code, with GLOBALVARS for free temps) Diddled (Larry Masinter's reworking using local lambda binding for temporaries) Version: CB (current release CONBRIO), WD (WIND system) Options: DD (display "down", or off), DU (display "up") 1st (first run), nth ("mode", or most frequently observed after first) All measurements in seconds. Timings on SYBAL,NB,CB,DD were also reproduced quite closely on Larry Masinter's machine, and on Stu Card's. Display Up vs. Display Down times ----------------------------------------------------------------- Swap 3.6 GSN | Swap 3.0 GSN July 2 GC 66.4 OB | GC 49. OB CPU 415. CB,DU,nth | CPU 299. CB,DD,nth Swap 33.1 GSN | Swap 5.7 GSN July 2 GC 70.0 diddled | GC 50.9 diddled CPU 305. CB,DU,1st | CPU 210. CB,DD,nth Swap 0.5 JONL | Swap - JONL July 2 GC 60. diddled | GC 30.2 diddled CPU 158. WD,DU,nth | CPU 116. WD,DD,nth Swap - SYBAL | Swap - SYBAL July 7 GC 56. diddled | GC 39.6 diddled CPU 204. CB,DU,nth | CPU 143. CB,DD,nth First run vs. nth ("mode") run; Display Down ----------------------------------------------------------------- Swap 2. JONL | Swap - JONL July 7 GC 26.7 NB | GC 31.6 NB CPU 142. CB,DD,1st | CPU 117. CB,DD,nth Swap .2 JONL | Swap - JONL July 7 GC 24.9 NB | GC 28.2 NB CPU 119. WD,DD,1st | CPU 107. WD,DD,nth Swap 9.8 SYBAL | Swap - SYBAL July 7 GC 31. NB | GC 35. NB CPU 140. CB,DD,1st | CPU 132. CB,DD,nth Swap .14 SYBAL | Swap - SYBAL July 7 GC 20.6 NB | GC 31.7 NB CPU 133. WD,DD,1st | CPU 119. WD,DD,nth Swap .1 SYBAL | Swap - SYBAL July 7 GC 33.2 diddled | GC 35. diddled CPU 150. WD,DD,1st | CPU 130. WD,DD,nth Dorado time ----------------------------------------------------------------- Swap ? Finisterra | Swap - Finisterra July 2 GC 11.4 diddled | GC 17. diddled CPU 25.6 WD,1st | CPU 22.7 WD,nth The STATS file mentioned for Dorado analysis is on the PHYLUM file server at PARC, file <JONL>TEST.PRINTOUT. Since it's a lengthy account of an incomplete run, I didn't reproduce it here. Mail-from: ARPANET site SU-SCORE rcvd at 8-Jul-82 1245-CDT Date: 8 Jul 1982 1043-PDT From: Gordon Novak <CSD.NOVAK at SU-SCORE> To: Masinter at PARC-MAXC, CL.BOYER at UTEXAS-20 cc: JonL at PARC-MAXC In-Reply-To: Your message of 7-Jul-82 1812-PDT Date: Thursday, 8 July 1982 12:43-CDT From: Gordon Novak <CSD.NOVAK at SU-SCORE> To: Masinter at PARC-MAXC, CL.BOYER cc: JonL at PARC-MAXC I reran the test as Larry did, with similar results (included below). My problem was that I used TCOMPL instead of BCOMPL. I recall being told by someone that the Dolphin didn't block-compile like Interlisp-10, so that BCOMPL and TCOMPL did the same thing. Obviously that isn't true; I should have been more careful. I apologize for raising a ruckus over a silly mistake; at least I'm glad that the results will be fair to the Dolphin crowd. DISPLAYDOWN, as used in Larry's test, totally turns off the display for the duration. I haven't used it myself, but I understand that it can get one into funny problemsif e.g. there are errors in the execution of the program with the display off; I don't know if most users would find it acceptable to run in this mode. NIL Mail-from: ARPANET site PARC-MAXC rcvd at 13-Jul-82 0217-CDT From: JonL at PARC-MAXC To: CL.BOYER cc: JonL at PARC-MAXC Re: Timings Table for IREWRITE benchmark Yes, the SYBAL,NB,CB,DD is an appropriate time for the current "vanilla" Dolphin; but the Dorado timing I reported in the previous note can't be strictly compared with the others since it was running the "diddled" test rather than the NewBoyer (NB) test, and was in the WIND release rather than CONBRIO. [As it happens, the "diddling" had somewhat of a misfeature in it, which is why I mentioned that NB is a much better benchmark anyway]. Dorado Frontenac, NewBoyer.benchmark(NB),systemCONBRIO(CB) DisplayDown (DD) times for "mode" (nth) run: GC = 10.9 CPU = 17.6 DisplayUp (DU) times for "mode" (nth) run: GC = 11.8 CPU = 19.2 DisplayDown (DD) times for "FirstRun" (1st) run: Swap = .027 GC = 10.5 CPU = 17.4 It's not clear to me why the "FirstRun" time was faster in these trials -- chalk it up to "noise", or maybe to the benefits of larger-memory/faster-disk? ∨ ←LOAD(IREWRITE.DCOM) compiled on 8-JUL-82 09:54:44 FILE CREATED 5-Jul-82 12:52:49 IREWRITECOMS {DSK}IREWRITE.DCOM;2 ←(DISPLAYDOWN (TIMEALL (SETUP))) Elapsed Time = .755 seconds SWAP time = .582 seconds CPU Time = .173 seconds PAGEFAULTS = 12 LISTP 224 T ←(DISPLAYDOWN '(TIMEALL (TEST))) Elapsed Time = 175.0 seconds SWAP time = 6.63 seconds GC time = 31.5 seconds CPU Time = 137.0 seconds PAGEFAULTS = 610 SWAPWRITES = 157 FIXP LISTP 311 226469 (T 168388 31471) ←REDO Elapsed Time = 183.0 seconds SWAP time = .494 seconds GC time = 48.7 seconds CPU Time = 134.0 seconds PAGEFAULTS = 21 FIXP LISTP 375 226469 (T 182913 48703) ←REDO Elapsed Time = 188.0 seconds SWAP time = .078 seconds GC time = 52.3 seconds CPU Time = 136.0 seconds PAGEFAULTS = 2 FIXP LISTP 419 226469 (T 188209 52257) ←REDO Elapsed Time = 188.0 seconds SWAP time = .015 seconds GC time = 51.2 seconds CPU Time = 137.0 seconds PAGEFAULTS = 14 FIXP LISTP 401 226469 (T 187906 51188) ←TIMEALL((TEST)) Elapsed Time = 271.0 seconds SWAP time = .059 seconds GC time = 75.3 seconds CPU Time = 195.0 seconds PAGEFAULTS = 1 FIXP LISTP 420 226469 (T 270715 75315) ←TIMEALL((TEST)) Elapsed Time = 267.0 seconds SWAP time = .006 seconds GC time = 73.2 seconds CPU Time = 194.0 seconds PAGEFAULTS = 6 FIXP LISTP 402 226469 (T 267145 73153) ←TIMEALL((TEST)) Elapsed Time = 266.0 seconds GC time = 72.6 seconds CPU Time = 194.0 seconds FIXP LISTP 402 226469 (T 266215 72623) ←DRIBBLE] ∨ The INTERLISP VAX test Mail-from: ARPANET site USC-ISIB rcvd at 23-Jul-82 1108-CDT Date: 23 Jul 1982 0907-PDT Sender: RBATES at USC-ISIB Subject: Re: lisp comparison. From: Raymond Bates <RBATES at ISIB> To: CL.BOYER at UTEXAS-20 Cc: CMP.GOOD at UTEXAS-20, ddyer at USC-ISIB, lynch at USC-ISIB, Cc: Novak at SUMEX-AIM Message-ID: <[USC-ISIB]23-Jul-82 09:07:07.RBATES> In-Reply-To: Your message of Thursday, 22 July 1982 13:12-CDT *** EOOH *** Date: Friday, 23 July 1982 11:07-CDT From: Raymond Bates <RBATES at ISIB> Sender: RBATES at USC-ISIB To: CL.BOYER cc: CMP.GOOD, ddyer at USC-ISIB, lynch at USC-ISIB, Novak at SUMEX-AIM Re: lisp comparison. Here is the DRIBBLE file of a long run: NIL 4←(GCGAG NIL] 40 5←LOAD(IREWRITE.v] compiled on 22-JUL-82 09:22:17 File Created: 5-Jul-82 12:52:49 % warning! this file possibly incompatible! Compiled by version 3.0 but current version is 2.1 IREWRITECOMS /lisp/rbates/lisp/IREWRITE.v;2 6←(SETUP] T 7←(FOR I FROM 1 TO 20 DO (PRINT (TEST ] (T 76048 0) (T 76464 0) (T 76496 0) (T 76272 0) (T 89072 4784) (T 80992 0) (T 81840 0) (T 81600 0) (T 90512 4752) (T 81904 0) (T 82032 0) (T 81248 0) (T 90512 5456) (T 80768 0) (T 80800 0) (T 80656 0) (T 91424 5456) (T 82112 0) (T 82384 0) (T 82432 0) NIL 8←(DRIBBLE] You many wonder why the cpu time has an extra 10 seconds each time the system does a gc. The reason is that the system has to re-hash all the hash array after the gc and time is being charge to the computation time and not gc time (we will fix that). This test was done on our 780. Any thing else you would like to see or known? /Ray ∨ ←LOAD(boyer.v] compiled on 14-AUG-84 16:41:34 File Created: 5-JUL-83 21:34:28 BOYERCOMS /lisp/rbates/lisp/dick/BOYER.V ←(TIME (SETUP] 224 conses 0.032 seconds T ←(TIME (TEST] 226497 conses 53.28 seconds (T 53648 0) ;;; SAIL (fasload boyer) (timit) Timing performed on Wednesday 09/15/82 at 10:50:58. Cpu Time = 7.635 Elapsed Time = 726.53333 Wholine Time = 241.866667 GC Time = 120.472 Load Average Before = 6.1742424 Load Average After = 2.85985446 Average Load Average = 4.5170484 NIL Timing performed on Wednesday 09/15/82 at 11:03:27. Cpu Time = 7.49 Elapsed Time = 65.0 Wholine Time = 36.4166665 GC Time = 12.669 Load Average Before = 2.54934967 Load Average After = 2.2733817 Average Load Average = 2.4113657 NIL Timing performed on Wednesday 09/15/82 at 11:04:44. Cpu Time = 7.509 Elapsed Time = 59.3166666 Wholine Time = 32.866667 GC Time = 11.513 Load Average Before = 2.17366004 Load Average After = 2.06962526 Average Load Average = 2.12164265 NIL ;;; SAIL (FIXSW T) (fasload boyer) (timit) Timing performed on Wednesday 09/15/82 at 11:06:16. Cpu Time = 7.629 Elapsed Time = 1076.21666 Wholine Time = 229.366667 GC Time = 120.4 Load Average Before = 1.81269705 Load Average After = 8.4301555 Average Load Average = 5.1214263 NIL Timing performed on Wednesday 09/15/82 at 11:24:17. Cpu Time = 7.494 Elapsed Time = 86.016666 Wholine Time = 36.733333 GC Time = 12.692 Load Average Before = 8.2354884 Load Average After = 5.64889336 Average Load Average = 6.9421909 NIL Timing performed on Wednesday 09/15/82 at 11:25:45. Cpu Time = 7.484 Elapsed Time = 82.3 Wholine Time = 33.983333 GC Time = 11.519 Load Average Before = 5.58177483 Load Average After = 4.12152493 Average Load Average = 4.8516499 NIL New CPU (fasload boyer) (timit) Timing performed on Thursday 01/26/84 at 13:09:55. Cpu (- GC) Time = 6.569 Elapsed Time = 174.383333 Wholine Time = 152.083334 GC Time = 109.592 Load Average Before = 0.314615965 Load Average After = 0.88344371 Average Load Average = 0.59902984 NIL Timing performed on Thursday 01/26/84 at 13:13:03. Cpu (- GC) Time = 6.469 Elapsed Time = 25.2833333 Wholine Time = 23.5 GC Time = 11.594 Load Average Before = 0.81077862 Load Average After = 0.85254848 Average Load Average = 0.83166355 NIL ;;; Boyer D2 7/5/83 Without interrupts SETUP: Elapsed .839 Swap .732 CPU .107 pgflts 21 dskops 18 TEST: Elapsed 132.0 GC 31.3 CPU 101.0 pgflts 554 swpwrts 76 dskops 76 D3 7/5/83 with interrupts, jonl env SETUP: Elapsed .034 Swap .014 CPU .02 pgflts 3 TEST: Elapsed 44.0 GC 17.0 pgflts 520 swpwrts 113 dskops 113 with interrupts, bare env TEST: Elapsed 30.3 GC 13.2 CPU 17.1 pgflts 2 D1 1/25/84 with interrupts TEST: Elapsed 119.0 CPU 74.6 GC 44.4 ;;; NIL ;;; Friday July 22,1983 2:16 FQ+4D.16H.41M.10S. -*- Text -*- BOYER Pass 1. Changes to preserve semantics: (member x y) => (member x y :test #'equal) try 1: cpu=116.5, elapsed=119.9, pagefaults=3907 Try 2: cpu=115.76, elapsed=120.70, pagefaults=3961 Note... I ran this part several times while experimenting with getting VMS to let me have the machine to myself (and not play musical pages with me). As i have noticed before, the times vary; in this case, from as little as 114 seconds (surprisingly, on one which paged more), to the 120 here (again surprisingly, which was set to page less). ---------------- Pass 2. Change, in TRANS-OF-IMPLIES1, (EQUAL N 1) -> (EQL N 1). Turn ON open-compilation of CAR, CDR, RPLACA, etc. Try 1: cpu=81.33,elapsed=83.78,pagefaults=3965 Try 2: cpu=81.69,elapsed=85.11,pagefaults=3993 ---- Comments. Heavy on function calls; this will show in NIL. Probably heavy on use of EQUAL. The NIL EQUAL function leaves much to be desired in efficiency (partly from function calls), especially in the simple cases. EQUAL is probably going to be written in macro-32 soon, to handle the simple cases. ;;; FRANZ ∂06-Jun-83 1039 RPG boyer ∂01-Jun-83 2251 jkf%UCBKIM@Berkeley boyer Received: from UCB-VAX by SU-AI with TCP/SMTP; 1 Jun 83 22:45:09 PDT Date: 1 Jun 83 22:46:28 PDT (Wed) From: jkf%UCBKIM@Berkeley (John Foderaro) Subject: boyer Message-Id: <8306020546.13350@UCBKIM.ARPA> Received: by UCBKIM.ARPA (3.340/3.5) id AA13350; 1 Jun 83 22:46:28 PDT (Wed) Received: from UCBKIM.ARPA by UCBVAX.ARPA (3.341/3.31) id AA10232; 1 Jun 83 22:45:39 PDT (Wed) To: rpg@su-ai (780cpu,gc)/(750cpu,gc) [seconds] >>> boyer: test translinks on off localf 21.33,50.42/36.18,82.35 21.3,21.32/36.15,35.01 compiled 40.13,50.43/62.38,78.68 137.85,21.25/223.47,34.5 interpreted 1061.02,32.25/1699.95,51.77 1058.88,22.47/1685.92,36.73 **** New Franz ∂09-Oct-83 0937 jkf@ucbkim boyer Received: from UCBKIM by SU-AI with TCP/SMTP; 9 Oct 83 09:37:37 PDT Received: by ucbkim.ARPA (4.6/4.2) id AA17661; Sun, 9 Oct 83 09:41:06 PDT Date: Sun, 9 Oct 83 09:41:06 PDT From: John Foderaro (on an h19-u) <jkf@ucbkim> Message-Id: <8310091641.AA17661@ucbkim.ARPA> To: rpg@su-ai Subject: boyer Cc: --- Benchmark boyer run on ucbkim at Sat Oct 8 02:45:06 PDT 1983 by jkf --- cpu usage: 2:45am up 3:15, 0 users, load average: 1.12, 1.13, 1.15 Franz Lisp, Opus 38.81 => [fasl boyer.o] t => benchmark: test (file boyer) , tranlinks: on, localf: no executing form: (test) begin (217 213) end (4507 2093) runs 1 avg cpu time 40.16666666666667, avg gc time 31.33333333333333 benchmark: test (file boyer) , tranlinks: off, localf: no executing form: (test) begin (4507 2093) end (14485 3372) runs 1 avg cpu time 144.9833333333333, avg gc time 21.31666666666667 nil => Franz Lisp, Opus 38.81 => [fasl boyer-l.o] t => benchmark: test (file boyer) , tranlinks: on, localf: yes executing form: (test) begin (208 211) end (3308 2076) runs 1 avg cpu time 20.58333333333333, avg gc time 31.08333333333333 benchmark: test (file boyer) , tranlinks: off, localf: yes executing form: (test) begin (3310 2076) end (5851 3357) runs 1 avg cpu time 21.0, avg gc time 21.35 nil => Franz Lisp, Opus 38.81 => [load boyer.l] [fasl benchmac.o] [fasl benchmac.o] t => benchmark: test (file boyer) , tranlinks: on, interpreted executing form: (test) begin (304 247) end (63663 2112) runs 1 avg cpu time 1024.9, avg gc time 31.08333333333333 benchmark: test (file boyer) , tranlinks: off, interpreted executing form: (test) begin (63665 2112) end (126963 3672) runs 1 avg cpu time 1028.966666666667, avg gc time 26.0 nil => --- cpu usage: 3:29am up 3:59, 0 users, load average: 1.31, 1.14, 1.12 --- end of benchmark boyer --- Benchmark boyer run on ucbmatisse at Fri Oct 7 18:16:45 PDT 1983 by jkf --- cpu usage: 6:16pm up 2:46, 1 users, load average: 1.21, 0.50, 0.29 Franz Lisp, Opus 38.81 => [fasl boyer.o] t => benchmark: test (file boyer) , tranlinks: on, localf: no executing form: (test) begin (400 273) end (7087 3327) runs 1 avg cpu time 60.55, avg gc time 50.9 benchmark: test (file boyer) , tranlinks: off, localf: no executing form: (test) begin (7089 3327) end (22613 5409) runs 1 avg cpu time 224.0333333333333, avg gc time 34.7 nil => Franz Lisp, Opus 38.81 => [fasl boyer-l.o] t => benchmark: test (file boyer) , tranlinks: on, localf: yes executing form: (test) begin (385 268) end (5505 3327) runs 1 avg cpu time 34.35, avg gc time 50.98333333333333 benchmark: test (file boyer) , tranlinks: off, localf: yes executing form: (test) begin (5507 3327) end (9689 5429) runs 1 avg cpu time 34.66666666666667, avg gc time 35.03333333333333 nil => Franz Lisp, Opus 38.81 => [load boyer.l] [fasl benchmac.o] [fasl benchmac.o] t => benchmark: test (file boyer) , tranlinks: on, interpreted executing form: (test) begin (486 273) end (99686 3314) runs 1 avg cpu time 1602.65, avg gc time 50.68333333333333 benchmark: test (file boyer) , tranlinks: off, interpreted executing form: (test) begin (99691 3314) end (197940 5422) runs 1 avg cpu time 1602.35, avg gc time 35.13333333333333 nil => --- cpu usage: 7:24pm up 3:54, 0 users, load average: 1.00, 1.03, 1.04 --- end of benchmark boyer --- Benchmark boyer run on ucbmike at Fri Oct 7 14:40:16 PDT 1983 by jkf --- cpu usage: 2:40pm up 5:12, 0 users, load average: 1.14, 1.05, 1.04 Franz Lisp, Opus 38.79 -> [fasl boyer.o] t -> benchmark: test (file boyer) , tranlinks: on, localf: no executing form: (test) begin (469 450) end (8861 4979) runs 1 avg cpu time 64.38333333333334, avg gc time 75.48333333333333 benchmark: test (file boyer) , tranlinks: off, localf: no executing form: (test) begin (8866 4979) end (26752 8086) runs 1 avg cpu time 246.3166666666667, avg gc time 51.78333333333333 nil -> Franz Lisp, Opus 38.79 -> [fasl boyer-l.o] t -> benchmark: test (file boyer) , tranlinks: on, localf: yes executing form: (test) begin (458 441) end (7517 4963) runs 1 avg cpu time 42.28333333333333, avg gc time 75.36666666666666 benchmark: test (file boyer) , tranlinks: off, localf: yes executing form: (test) begin (7522 4963) end (13188 8058) runs 1 avg cpu time 42.85, avg gc time 51.58333333333334 nil -> Franz Lisp, Opus 38.79 -> [load boyer.l] [fasl benchmac.o] [fasl benchmac.o] t -> benchmark: test (file boyer) , tranlinks: on, interpreted executing form: (test) begin (651 510) end (118177 5034) runs 1 avg cpu time 1883.366666666667, avg gc time 75.40000000000001 benchmark: test (file boyer) , tranlinks: off, interpreted executing form: (test) begin (118185 5034) end (234299 8116) runs 1 avg cpu time 1883.866666666667, avg gc time 51.36666666666667 nil -> --- cpu usage: 4:04pm up 6:35, 0 users, load average: 1.10, 1.06, 1.03 --- end of benchmark boyer ;;; SCORE Oct 18, 1983 LISP LOAD(BOYER) MAKEFILE(BOYER) CLEANUP) BCOMPL(BOYER) ST (SETUP) (TIME (TEST) 1 3) (TIME (TEST) 1 3) collecting lists 8974, 10510 free cells collecting lists 9127, 10151 free cells collecting lists 9346, 10370 free cells collecting lists 1655, 10359 free cells collecting lists 2054, 10246 free cells collecting lists 7526, 10086 free cells collecting lists 7204, 10276 free cells collecting lists 7256, 10328 free cells collecting lists 9076, 10100 free cells collecting lists 6754, 10338 free cells collecting lists 7772, 10332 free cells collecting lists 7768, 10328 free cells collecting lists 6910, 10494 free cells collecting lists 7584, 10144 free cells collecting lists 8692, 10228 free cells collecting lists 7188, 10260 free cells collecting lists 11498, 11498 free cells collecting lists 8254, 10302 free cells collecting lists 7180, 10252 free cells, 36 pages left collecting lists 7254, 10326 free cells, 30 pages left collecting lists 8952, 10488 free cells, 27 pages left collecting lists 8470, 10006 free cells, 24 pages left 226469 conses 25.458 seconds 27.479 seconds, garbage collection time (T 52933 27479) ← ;;; DEC780CL cpu + probability x gc BOYER 55 + 1.3 x 22 ************************************************************************* Name of VAXLisp VAXLisp VAXLisp VAXLisp application U1.0-20 U1.0-20 U1.0-20 U1.0-20 Benchmark VMS V3.5 VMS V3.5 VMS V3.5 VMS V3.6 730 (No FPA) 750 (No FPA) 780 785 (No FPA) ------------------------------------------------------------------------------- ------------------------------------------------------------------------------- Boyer 258.98 69.38 46.79 30.36 (GC 180.82) (GC 79.30) (GC 40.90) (GC 28.38) ;;; InterLisp Vax 780 BOYER: ←(TIME (SETUP] 224 conses 0.096 seconds T ←(TIME (TEST] 226500 conses 64.928 seconds (T 64928 0) ;;; PSL-20 3.3 Boyer Test Timing performed on DEC-20 23-Mar-84 05:03:37 . *** Garbage collection starting *** GC 4: time 4833 ms, 179307 recovered, 179307 free *** Garbage collection starting *** GC 5: time 6772 ms, 140848 recovered, 140849 free ........................................ Cpu (- GC) Time = 11.96 secs Elapsed Time = 27.0 secs GC Time = 11.605 secs Load Average Before = 1.2 Load Average After = 1.1 Average Load Average = 1.15 ;;; PSL-cray 3.2 ;;; Times are in milliseconds 08:17:58 000:55.847 Boyer Test 08:19:08 001:23.710 Cpu (- GC) Time = 1852.68500000 secs$2 ε 08:19:10 001:24.230 Elapsed Time = 0. secs 08:19:11 001:24.751 GC Time = 7592.79600000 secs$2 ε 08:19:13 001:25.272 Load Average Before = 0 08:19:15 001:25.792 Load Average After = 0 08:19:16 001:26.312 Average Load Average = 0. Boyer Test Timing performed on CRAY 23-apr-84 12:00:00. ........................................ Cpu (- GC) Time = 1874.67800000 secs Elapsed Time = 0. secs GC Time = 1509.07900000 secs Load Average Before = 0 Load Average After = 0 Average Load Average = 0. ;;; PSL-750 3.2 Cpu (- GC) Time = 43.384 secs Elapsed Time = 0.0 secs GC Time = 40.715 secs Load Average Before = 0 Load Average After = 0 Average Load Average = 0.0 ;;; PSL-780 3.2 Cpu (- GC) Time = 21.301 secs Elapsed Time = 0.0 secs GC Time = 19.975 secs Load Average Before = 0 Load Average After = 0 Average Load Average = 0.0 ;;; PSL-dn600 Cpu (- GC) Time = 43.7 secs Elapsed Time = 0.0 secs GC Time = 41.184 secs Load Average Before = 0 Load Average After = 0 Average Load Average = 0.0 ;;; PSL-dn300 Cpu (- GC) Time = 46.924 secs Elapsed Time = 0.0 secs GC Time = 48.585 secs Load Average Before = 0 Load Average After = 0 Average Load Average = 0.0 ;;; PSL-dn160 Boyer Test Timing performed on Apollo today 12:00:00. ........................................ Cpu (- GC) Time = 25.663 secs Elapsed Time = 0.0 secs GC Time = 15.349 secs Load Average Before = 0 Load Average After = 0 Average Load Average = 0.0 ;;; PERQ 6/18/84 195.43 seconds (stopwatch) 7/31/84 Benchmark % of old time Time Machine used Boyer 82% 159.80 Skef's T1 ;;; PSL Numbers 7/31/84 |KL-10b| 20-60 | 20-60 | 3600 | 20-60 | CRAY | 12Mhz| HP-UX Benchmark |MACLSP|InterLsp|PSL 3.2| ZetaL|PSL 3.3|PSL3.2| HP200|PSL3.3 -------------------------------------------------------------------------- Boyer | 6.47| 25.458| 11.74 | 12 | 11.87| 1.905| 25.52| 25.19 ;;; LMI/Tyson 15-Aug-84 1920 Timing 1 Timing 2 Boyer 53.7 (5.8) 50.8 (3.9) ;;; LMI/Carrette 9-4-84 Test MacroCompiled Microcompiled BOYER 31.7 13.2 ;;; S-1 August 21, 1984 10.03 ;;; 3600 Sept 12, 1984 Real, no IFU Real, IFU Ratio CPU, no IFU CPU, IFU Ratio Boyer 18.57 15.87 1.17 18.49 14.60 1.27