Changed the array usage checking to always include equations involving replicators
This allows us to check situations like this:
PAR i = 0 FOR 10
IF
i = 0
a[10] := 3
TRUE
a[i] := 3
Previously this would have been flagged unsafe (because 10 can overlap with 10 between the replicated branches).
But with this change, the equations on the replicators (including: i'>=i+1, i = 0, i' = 0) are included alongside 10=10, so there is no solution over all because the replicator equations prevent a solution (i.e. the 10 can't be used twice in parallel).
This commit is contained in:
Neil Brown
parent
f1cc74e88e
commit
2ecd91e36f
|
|
@ -1,6 +1,6 @@
|
|||
{-
|
||||
Tock: a compiler for parallel languages
|
||||
Copyright (C) 2007 University of Kent
|
||||
Copyright (C) 2007--2009 University of Kent
|
||||
|
||||
This program is free software; you can redistribute it and/or modify it
|
||||
under the terms of the GNU General Public License as published by the
|
||||
|
|
@ -266,15 +266,17 @@ parItemToArrayAccessM :: Monad m =>
|
|||
m [(label, ArrayAccessType, (EqualityConstraintEquation, EqualityProblem, InequalityProblem))]
|
||||
) ->
|
||||
ParItems a ->
|
||||
m [ArrayAccess label]
|
||||
m ([ArrayAccess label], [A.Name])
|
||||
parItemToArrayAccessM f (SeqItems xs)
|
||||
-- Each sequential item is a group of one:
|
||||
= sequence [concatMapM (f []) xs >>* Group]
|
||||
parItemToArrayAccessM f (ParItems ps) = concatMapM (parItemToArrayAccessM f) ps
|
||||
= do aas <- sequence [concatMapM (f []) xs >>* Group]
|
||||
return (aas, [])
|
||||
parItemToArrayAccessM f (ParItems ps)
|
||||
= liftM (transformPair concat concat . unzip) $ mapM (parItemToArrayAccessM f) ps
|
||||
parItemToArrayAccessM f (RepParItem rep p)
|
||||
= do normal <- parItemToArrayAccessM (\reps -> f ((rep,False):reps)) p
|
||||
mirror <- parItemToArrayAccessM (\reps -> f ((rep,True):reps)) p
|
||||
return [Replicated normal mirror]
|
||||
= do (normal, otherReps) <- parItemToArrayAccessM (\reps -> f ((rep,False):reps)) p
|
||||
mirror <- liftM fst $ parItemToArrayAccessM (\reps -> f ((rep,True):reps)) p
|
||||
return ([Replicated normal mirror], fst rep : otherReps)
|
||||
|
||||
-- | Turns a list of expressions (which may contain many constants, or duplicated variables)
|
||||
-- into a set of expressions with at most one constant term, and at most one appearance
|
||||
|
|
@ -403,16 +405,19 @@ accumProblem (a,b) (c,d) = (a ++ c, b ++ d)
|
|||
makeEquations :: ParItems (BK, [A.Expression], [A.Expression]) -> A.Expression ->
|
||||
Either String [(((A.Expression, [ModuloCase]), (A.Expression, [ModuloCase])), VarMap, (EqualityProblem, InequalityProblem))]
|
||||
makeEquations accesses bound
|
||||
= do ((v,h,repVarIndexes),s) <- (flip runStateT) Map.empty $
|
||||
do (accesses',repVars) <- flip runStateT [] $ parItemToArrayAccessM mkEq accesses
|
||||
= do ((v,h,repVarIndexes, allReps),s) <- (flip runStateT) Map.empty $
|
||||
do ((accesses', allReps),repVars) <- flip runStateT [] $ parItemToArrayAccessM mkEq accesses
|
||||
high <- makeSingleEq id bound "upper bound"
|
||||
return (accesses', high, nub repVars)
|
||||
return $ squareAndPair lookupBK (\(x,y,_) -> (x,y)) repVarIndexes s v (amap (const 0) h, addConstant (-1) h)
|
||||
return (accesses', high, nub repVars, allReps)
|
||||
return $ squareAndPair (lookupBK allReps) (\(x,y,_) -> (x,y)) repVarIndexes s v (amap (const 0) h, addConstant (-1) h)
|
||||
|
||||
where
|
||||
lookupBK :: (A.Expression, [ModuloCase], BK') -> [(EqualityProblem, InequalityProblem)]
|
||||
lookupBK (e,_,bk) = map (foldl accumProblem ([],[]) . map snd . filter (\(v,eq) -> v `elem` vs) . Map.toList) bk
|
||||
lookupBK :: [A.Name] -> (A.Expression, [ModuloCase], BK') -> [(EqualityProblem, InequalityProblem)]
|
||||
lookupBK reps (e,_,bk) = map (foldl accumProblem ([],[]) . map snd .
|
||||
filter (\(v,eq) -> v `elem` vs || v `elem` reps') . Map.toList) bk
|
||||
where
|
||||
reps' :: [Var]
|
||||
reps' = map (Var . A.Variable emptyMeta) reps
|
||||
vs :: [Var]
|
||||
vs = map Var $ listify (const True :: A.Variable -> Bool) e
|
||||
|
||||
|
|
@ -631,12 +636,8 @@ squareAndPair lookupBK strip repVars s v lh
|
|||
|
||||
addExtra :: (CoeffIndex, CoeffIndex) -> (EqualityProblem,InequalityProblem) -> InequalityProblem
|
||||
addExtra (plain,prime) (eq, ineq)
|
||||
| itemPresent plain (eq ++ ineq) && itemPresent prime (eq ++ ineq) = extraIneq
|
||||
| otherwise = []
|
||||
where
|
||||
extraIneq :: InequalityProblem
|
||||
-- prime >= plain + 1 (prime - plain - 1 >= 0)
|
||||
extraIneq = [mapToArray $ Map.fromList [(prime,1), (plain,-1), (0, -1)]]
|
||||
-- prime >= plain + 1 (prime - plain - 1 >= 0)
|
||||
= [mapToArray $ Map.fromList [(prime,1), (plain,-1), (0, -1)]]
|
||||
|
||||
getSingleAccessItem :: MonadTrans m => String -> ArrayAccess label -> m (Either String) EqualityConstraintEquation
|
||||
getSingleAccessItem _ (Group [(_,_,(acc,_,_))]) = lift $ return acc
|
||||
|
|
|
|||
|
|
@ -375,27 +375,26 @@ testMakeEquations = TestLabel "testMakeEquations" $ TestList
|
|||
("i", intLiteral 1, intLiteral 6),[exprVariable "i"],intLiteral 8)
|
||||
|
||||
-- i vs i' vs 3
|
||||
,testRep' (201,
|
||||
,let common = ij_16 &&& [i <== j ++ con (-1)] in testRep' (201,
|
||||
[(((0,[]),(0,[])),rep_i_mapping, [i === j],
|
||||
ij_16 &&& [i <== j ++ con (-1)]
|
||||
&&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])]
|
||||
++ replicate 2 (((0,[]),(1,[])),rep_i_mapping,[i === con 3], leq [con 1,j, con 6] &&&
|
||||
leq [con 1,i, con 6] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7])
|
||||
++ [(((1,[]),(1,[])),rep_i_mapping,[con 3 === con 3],concat $ replicate 2 (leq [con 0, con 3, con 7]))]
|
||||
common &&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])]
|
||||
++ replicate 2 (((0,[]),(1,[])),rep_i_mapping,[i === con 3], common
|
||||
&&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7])
|
||||
++ [(((1,[]),(1,[])),rep_i_mapping,[con 3 === con 3],common &&& (concat $ replicate 2 (leq [con 0, con 3, con 7])))]
|
||||
,("i", intLiteral 1, intLiteral 6),[exprVariable "i", intLiteral 3],intLiteral 8)
|
||||
|
||||
-- i vs i + 1 vs i' vs i' + 1
|
||||
,testRep' (202,[
|
||||
(((0,[]),(1,[])),rep_i_mapping,[i === j ++ con 1],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, j ++ con 1, con 7])
|
||||
,(((0,[]),(1,[])),rep_i_mapping,[i ++ con 1 === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j, con 7])
|
||||
,(((0,[]),(0,[])),rep_i_mapping,[i === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])
|
||||
,(((1,[]),(1,[])),rep_i_mapping,[i === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j ++ con 1, con 7])]
|
||||
++ [(((0,[]),(1,[])),rep_i_mapping, [i === i ++ con 1], leq [con 1, i, con 6] &&& leq [con 1, j, con 6] &&&
|
||||
,let common = ij_16 &&& [i <== j ++ con (-1)] in testRep' (202,[
|
||||
(((0,[]),(1,[])),rep_i_mapping,[i === j ++ con 1],common &&& leq [con 0, i, con 7] &&& leq [con 0, j ++ con 1, con 7])
|
||||
,(((0,[]),(1,[])),rep_i_mapping,[i ++ con 1 === j],common &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j, con 7])
|
||||
,(((0,[]),(0,[])),rep_i_mapping,[i === j],common &&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])
|
||||
,(((1,[]),(1,[])),rep_i_mapping,[i === j],common &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j ++ con 1, con 7])]
|
||||
++ [(((0,[]),(1,[])),rep_i_mapping, [i === i ++ con 1], common &&&
|
||||
leq [con 0, i, con 7] &&& leq [con 0,i ++ con 1, con 7])]
|
||||
,("i", intLiteral 1, intLiteral 6),[exprVariable "i", buildExpr $ Dy (Var "i") A.Add (Lit $ intLiteral 1)],intLiteral 8)
|
||||
|
||||
-- Only a constant:
|
||||
,testRep' (210,[(((0,[]),(0,[])),rep_i_mapping,[con 4 === con 4],concat $ replicate 2 $ leq [con 0, con 4, con 7])]
|
||||
,testRep' (210,[(((0,[]),(0,[])),rep_i_mapping,[con 4 === con 4],ij_16 &&& [i <== j ++ con (-1)] &&& (concat $ replicate 2 $ leq [con 0, con 4, con 7]))]
|
||||
,("i", intLiteral 1, intLiteral 6),[intLiteral 4],intLiteral 8)
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -107,6 +107,13 @@ PROC m()
|
|||
a[k] := 1
|
||||
TRUE
|
||||
SKIP
|
||||
%PASS IF, safe indirectly over replication 3
|
||||
PAR k = 0 FOR 9
|
||||
IF
|
||||
k = 0
|
||||
a[9] := 3
|
||||
TRUE
|
||||
a[k] := 3
|
||||
%FAIL IF, unsafe indirectly over replication
|
||||
PAR k = 0 FOR 10
|
||||
IF
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user