From 6a42c8ef119e3a86cd853baebf6ddf07e1bea1fc Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Wed, 20 Apr 2016 11:25:45 +0200 Subject: [PATCH 1/3] performance optimization --- .../unify/MartelliMontanariUnify.java | 12 +-- .../unify/model/FiniteClosure.java | 80 ++++++++++--------- .../typeinference/unify/model/TypeParams.java | 13 ++- .../typeinference/unify/model/Unifier.java | 7 ++ .../typeinference/unify/model/UnifyPair.java | 11 ++- 5 files changed, 75 insertions(+), 48 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java b/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java index 80dabce6..1c75ea99 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java @@ -50,12 +50,6 @@ public class MartelliMontanariUnify implements IUnify { TypeParams rhsTypeParams = rhsType.getTypeParams(); TypeParams lhsTypeParams = lhsType.getTypeParams(); - // DELETE - Rule - if(pair.getRhsType().equals(pair.getLhsType())) { - termsList.remove(idx); - continue; - } - // REDUCE - Rule if(!(rhsType instanceof PlaceholderType) && !(lhsType instanceof PlaceholderType)) { Set result = new HashSet<>(); @@ -78,6 +72,12 @@ public class MartelliMontanariUnify implements IUnify { termsList.addAll(result); continue; } + + // DELETE - Rule + if(pair.getRhsType().equals(pair.getLhsType())) { + termsList.remove(idx); + continue; + } // SWAP - Rule if(!(lhsType instanceof PlaceholderType) && (rhsType instanceof PlaceholderType)) { diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java index 17fbb240..ac0862cc 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java @@ -106,10 +106,10 @@ public class FiniteClosure implements IFiniteClosure { // Permute all params with values that are in smArg() of that type. // This corresponds to Case 3 in the definition of the subtyping relation. - {ArrayList> paramCandidates = new ArrayList<>(); + /*{ArrayList> paramCandidates = new ArrayList<>(); for (UnifyType param : type.getTypeParams()) paramCandidates.add(smArg(param)); - permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));} + permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));}*/ // This is case 2 of the definition of the subtyping relation. Set result2 = new HashSet<>(); @@ -117,23 +117,24 @@ public class FiniteClosure implements IFiniteClosure { HashSet candidates = new HashSet<>(); // All types with the same name strInheritanceGraph.get(type.getName()).forEach(x -> candidates.add(x.getContent())); - for(UnifyType typePrime : result1) { - for (UnifyType theta2 : candidates) { - // Find the substitution - Optional sigma2Opt = unify.unify(typePrime, theta2); - if (!sigma2Opt.isPresent()) - continue; - Unifier sigma2 = sigma2Opt.get(); - sigma2.swapPlaceholderSubstitutions(typePrime.getTypeParams()); - if(type.equals(theta2)) - continue; - Set theta1s = smaller(theta2); - for (UnifyType theta1 : theta1s) { - // Because only the most general type is calculated, sigma1 = sigma2 - UnifyType sigma1Theta1 = sigma2.apply(theta1); - result2.add(sigma1Theta1); - } - } + //for(UnifyType typePrime : result1) { + for (UnifyType theta2 : candidates) { + // Find the substitution + Optional sigma2Opt = unify.unify(type, theta2); + if (!sigma2Opt.isPresent()) + continue; + Unifier sigma2 = sigma2Opt.get(); + if(sigma2.size() == 0) + continue; + sigma2.swapPlaceholderSubstitutions(type.getTypeParams()); + //if(type.equals(theta2)) + // continue; + Set theta1s = smaller(theta2); + for (UnifyType theta1 : theta1s) { + // Because only the most general type is calculated, sigma1 = sigma2 + UnifyType sigma1Theta1 = sigma2.apply(theta1); + result2.add(sigma1Theta1); + } } } else @@ -210,10 +211,10 @@ public class FiniteClosure implements IFiniteClosure { // Permute all params with values that are in smArg() of that type. // This corresponds to Case 3 in the definition of the subtyping relation. - {ArrayList> paramCandidates = new ArrayList<>(); + /*{ArrayList> paramCandidates = new ArrayList<>(); for (UnifyType param : type.getTypeParams()) paramCandidates.add(grArg(param)); - permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));} + permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));}*/ // This is case 2 of the definition of the subtyping relation. Set result2 = new HashSet<>(); @@ -221,24 +222,27 @@ public class FiniteClosure implements IFiniteClosure { HashSet candidates = new HashSet<>(); // All types with the same name strInheritanceGraph.get(type.getName()).forEach(x -> candidates.add(x.getContent())); - - for(UnifyType typePrime : result1) { - for (UnifyType theta2 : candidates) { - // Find the substitution - Optional sigma2Opt = unify.unify(typePrime, theta2); - if (!sigma2Opt.isPresent()) - continue; - if(type.equals(theta2)) - continue; - Unifier sigma2 = sigma2Opt.get(); - sigma2.swapPlaceholderSubstitutions(typePrime.getTypeParams()); - Set theta1s = greater(theta2); - for (UnifyType theta1 : theta1s) { - // Because only the most general type is calculated, sigma1 = sigma2 - UnifyType sigma1Theta1 = sigma2.apply(theta1); - result2.add(sigma1Theta1); - } + + // for(UnifyType typePrime : result1) + for (UnifyType theta2 : candidates) { + // Find the substitution + Optional sigma2Opt = unify.unify(type, theta2); + if (!sigma2Opt.isPresent()) + continue; + //if (type.equals(theta2)) + // continue; + Unifier sigma2 = sigma2Opt.get(); + if(sigma2.size() == 0) // type.equals(theta2) + continue; + sigma2.swapPlaceholderSubstitutions(type.getTypeParams()); + Set theta1s = greater(theta2); + for (UnifyType theta1 : theta1s) { + // Because only the most general type is calculated, sigma1 + // = sigma2 + UnifyType sigma1Theta1 = sigma2.apply(theta1); + result2.add(sigma1Theta1); } + // } } } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java index aa534b60..7ce251d9 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java @@ -15,6 +15,11 @@ public final class TypeParams implements Iterable{ */ private final UnifyType[] typeParams; + /** + * Hashcode calculation is expensive and must be cached. + */ + private final int hashCode; + /** * Creates a new set of type parameters. * @param types The type parameters. @@ -23,6 +28,9 @@ public final class TypeParams implements Iterable{ typeParams = new UnifyType[types.size()]; for(int i=0;i{ */ public TypeParams(UnifyType... types) { typeParams = types; + + // Hashcode calculation is expensive and must be cached. + hashCode = Arrays.hashCode(typeParams); } /** @@ -108,7 +119,7 @@ public final class TypeParams implements Iterable{ @Override public int hashCode() { - return Arrays.hashCode(typeParams); + return hashCode; } @Override diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java index 1a3988db..dbcc9b39 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java @@ -81,6 +81,13 @@ public class Unifier implements Function, Iterable b) in this unifier, * a is not an element of the targetParams. Substitutions that do not diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java index ed2c95ef..62de0c96 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java @@ -9,18 +9,20 @@ public class UnifyPair { /** * The type on the left hand side of the pair. */ - private UnifyType lhs; + private final UnifyType lhs; /** * The type on the right hand side of the pair. */ - private UnifyType rhs; + private final UnifyType rhs; /** * The operator that determines the relation between the left and right hand side type. */ private PairOperator pairOp; + private final int hashCode; + /** * Creates a new instance of the pair. * @param lhs The type on the left hand side of the pair. @@ -31,6 +33,9 @@ public class UnifyPair { this.lhs = lhs; this.rhs = rhs; pairOp = op; + + // Caching hashcode + hashCode = 17 + 31 * lhs.hashCode() + 31 * rhs.hashCode() + 31 * pairOp.hashCode(); } /** @@ -68,7 +73,7 @@ public class UnifyPair { @Override public int hashCode() { - return 17 + 31 * lhs.hashCode() + 31 * rhs.hashCode() + 31 * pairOp.hashCode(); + return hashCode; } @Override From 863bfa40d38380d805e064e00298bd88d399bec3 Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Wed, 20 Apr 2016 11:34:40 +0200 Subject: [PATCH 2/3] performance opt --- src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java index 805d461c..60e77536 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java @@ -58,7 +58,7 @@ public class TypeUnify { * Step 1: Repeated application of reduce, adapt, erase, swap */ Set eq0 = applyTypeUnificationRules(eq, fc); - + /* * Step 2 and 3: Create a subset eq1s of pairs where both sides are TPH and eq2s of the other pairs */ From 8780d5d47af33fc00bb5159c810c3e68827cd43a Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Wed, 20 Apr 2016 12:15:04 +0200 Subject: [PATCH 3/3] option for parallelization --- .../typeinference/unify/TypeUnify.java | 56 ++++++++++++++----- 1 file changed, 42 insertions(+), 14 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java index 60e77536..2e0d70fd 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java @@ -3,6 +3,7 @@ package de.dhbwstuttgart.typeinference.unify; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; +import java.util.Collections; import java.util.HashSet; import java.util.LinkedHashSet; import java.util.LinkedList; @@ -10,6 +11,7 @@ import java.util.List; import java.util.Map.Entry; import java.util.Optional; import java.util.Set; +import java.util.function.Function; import java.util.stream.Collectors; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; @@ -47,6 +49,8 @@ public class TypeUnify { */ protected IRuleSet rules = new RuleSet(); + protected boolean parallel = true; + /** * Computes all principal type unifiers for a set of constraints. * @param eq The set of constraints @@ -110,7 +114,7 @@ public class TypeUnify { // Sub cartesian products of the second level (pattern matched) sets // "the big (x)" - // TODO Optimierungsmöglichkeit: Parallelisierung der Schleife möglich + // TODO Optimierungsmöglichkeit: Parallelisierung der Schleife möglich (scheint sich nicht zu lohnen) for(Set>> secondLevelSet : secondLevelSets) { List>> secondLevelSetList = new ArrayList<>(secondLevelSet); Set>> cartResult = setOps.cartesianProduct(secondLevelSetList); @@ -133,7 +137,7 @@ public class TypeUnify { //System.out.println(result); // Flatten the cartesian product - // TODO parallelisierung möglich + // TODO parallelisierung möglich (scheint sich nicht zu lohnen) Set> eqPrimeSetFlat = new HashSet<>(); for(Set> setToFlatten : eqPrimeSet) { Set buffer = new HashSet<>(); @@ -148,15 +152,33 @@ public class TypeUnify { Set> restartSet = new HashSet<>(); Set> eqPrimePrimeSet = new HashSet<>(); - for(Set eqPrime : eqPrimeSetFlat) { - Optional> eqPrimePrime = rules.subst(eqPrime); + + if(parallel) { + Set> restartSetSync = Collections.synchronizedSet(restartSet); + Set> eqPrimePrimeSetSync = Collections.synchronizedSet(eqPrimePrimeSet); - if (eqPrime.equals(eq)) - eqPrimePrimeSet.add(eqPrime); - else if(eqPrimePrime.isPresent()) - restartSet.add(eqPrimePrime.get()); - else - restartSet.add(eqPrime); + eqPrimeSetFlat.parallelStream().forEach(eqPrime -> { + Optional> eqPrimePrime = rules.subst(eqPrime); + + if (eqPrime.equals(eq)) + eqPrimePrimeSetSync.add(eqPrime); + else if(eqPrimePrime.isPresent()) + restartSetSync.add(eqPrimePrime.get()); + else + restartSetSync.add(eqPrime); + }); + } + else { + for(Set eqPrime : eqPrimeSetFlat) { + Optional> eqPrimePrime = rules.subst(eqPrime); + + if (eqPrime.equals(eq)) + eqPrimePrimeSet.add(eqPrime); + else if(eqPrimePrime.isPresent()) + restartSet.add(eqPrimePrime.get()); + else + restartSet.add(eqPrime); + } } /* @@ -164,10 +186,16 @@ public class TypeUnify { * b) Build the union over everything */ // TODO parallelisierung möglich (lohnt sich vermutlich) - for(Set eqss : restartSet) - eqPrimePrimeSet.addAll(this.unify(eqss, fc)); - /*restartSet.parallelStream().forEach( - x -> eqPrimePrimeSet.addAll(unify(x, fc)));*/ + + if(parallel) { + Set> eqPrimePrimeSetSync = Collections.synchronizedSet(eqPrimePrimeSet); + restartSet.parallelStream().forEach( x -> eqPrimePrimeSetSync.addAll(unify(x, fc))); + } + else { + for(Set eqss : restartSet) + eqPrimePrimeSet.addAll(this.unify(eqss, fc)); + } + /* * Step 7: Filter empty sets; */