use types to partially prove correctness of journal locking code

My implementation does not guard against double locking of the journal. But
it does ensure that the journal is always locked when operated on, by using
a type that is only produced by lockJournal, and which is required as a
parameter of all functions that operate on the journal.

Note that I had to add the fooStale functions for cases where it does not
make sense to lock the journal when querying it. I was more concerned about
ensuring that anything that modifies the journal is locked.
setJournalFile's implementation ensures that any query of the journal will
get one value or the other atomically, even if the journal is being changed
at the time.

2 files changed, 68 insertions, 47 deletions

diff --git a/Annex/Branch.hs b/Annex/Branch.hs
index 9dfdaa876..f7b7f049a 100644
--- a/Annex/Branch.hs
+++ b/Annex/Branch.hs
@@ -136,33 +136,33 @@ updateTo pairs = do
 		{- Even when no refs need to be merged, the index
 		 - may still be updated if the branch has gotten ahead 
 		 - of the index. -}
-		then whenM (needUpdateIndex branchref) $ lockJournal $ do
+		then whenM (needUpdateIndex branchref) $ lockJournal $ \jl -> do
 			forceUpdateIndex branchref
 			{- When there are journalled changes
 			 - as well as the branch being updated,
 			 - a commit needs to be done. -}
 			when dirty $
-				go branchref True [] []
+				go branchref True [] [] jl
 		else lockJournal $ go branchref dirty refs branches
 	return $ not $ null refs
   where
 	isnewer ignoredrefs (r, _)
 		| S.member r ignoredrefs = return False
 		| otherwise = inRepo $ Git.Branch.changed fullname r
-	go branchref dirty refs branches = withIndex $ do
-		cleanjournal <- if dirty then stageJournal else return noop
+	go branchref dirty refs branches jl = withIndex $ do
+		cleanjournal <- if dirty then stageJournal jl else return noop
 		let merge_desc = if null branches
 			then "update"
 			else "merging " ++
 				unwords (map Git.Ref.describe branches) ++ 
 				" into " ++ show name
 		localtransitions <- parseTransitionsStrictly "local"
-			<$> getStale transitionsLog
+			<$> getLocal transitionsLog
 		unless (null branches) $ do
 			showSideAction merge_desc
 			mergeIndex refs
 		let commitrefs = nub $ fullname:refs
-		unlessM (handleTransitions localtransitions commitrefs) $ do
+		unlessM (handleTransitions jl localtransitions commitrefs) $ do
 			ff <- if dirty
 				then return False
 				else inRepo $ Git.Branch.fastForward fullname refs
@@ -181,21 +181,18 @@ updateTo pairs = do
 get :: FilePath -> Annex String
 get file = do
 	update
-	get' file
+	getLocal file
 
 {- Like get, but does not merge the branch, so the info returned may not
  - reflect changes in remotes.
  - (Changing the value this returns, and then merging is always the
  - same as using get, and then changing its value.) -}
-getStale :: FilePath -> Annex String
-getStale = get'
-
-get' :: FilePath -> Annex String
-get' file = go =<< getJournalFile file
+getLocal :: FilePath -> Annex String
+getLocal file = go =<< getJournalFileStale file
   where
 	go (Just journalcontent) = return journalcontent
 	go Nothing = getRaw file
-	
+
 getRaw :: FilePath -> Annex String
 getRaw file = withIndex $ L.unpack <$> catFile fullname file
 
@@ -205,16 +202,16 @@ getRaw file = withIndex $ L.unpack <$> catFile fullname file
  - modifes the current content of the file on the branch.
  -}
 change :: FilePath -> (String -> String) -> Annex ()
-change file a = lockJournal $ a <$> getStale file >>= set file
+change file a = lockJournal $ \jl -> a <$> getLocal file >>= set jl file
 
 {- Records new content of a file into the journal -}
-set :: FilePath -> String -> Annex ()
+set :: JournalLocked -> FilePath -> String -> Annex ()
 set = setJournalFile
 
 {- Stages the journal, and commits staged changes to the branch. -}
 commit :: String -> Annex ()
-commit message = whenM journalDirty $ lockJournal $ do
-	cleanjournal <- stageJournal
+commit message = whenM journalDirty $ lockJournal $ \jl -> do
+	cleanjournal <- stageJournal jl
 	ref <- getBranch
 	withIndex $ commitBranch ref message [fullname]
 	liftIO cleanjournal
@@ -236,6 +233,8 @@ commit message = whenM journalDirty $ lockJournal $ do
  - The branchref value can have been obtained using getBranch at any
  - previous point, though getting it a long time ago makes the race
  - more likely to occur.
+ -
+ - Should be called only inside lockJournal.
  -}
 commitBranch :: Git.Ref -> String -> [Git.Ref] -> Annex ()
 commitBranch branchref message parents = do
@@ -278,7 +277,7 @@ files = do
 	update
 	(++)
 		<$> branchFiles
-		<*> getJournalledFiles
+		<*> getJournalledFilesStale
 
 {- Files in the branch, not including any from journalled changes,
  - and without updating the branch. -}
@@ -369,13 +368,12 @@ setIndexSha ref = do
 
 {- Stages the journal into the index and returns an action that will
  - clean up the staged journal files, which should only be run once
- - the index has been committed to the branch. Should be run within
- - lockJournal, to prevent others from modifying the journal. -}
-stageJournal :: Annex (IO ())
-stageJournal = withIndex $ do
+ - the index has been committed to the branch. -}
+stageJournal :: JournalLocked -> Annex (IO ())
+stageJournal jl = withIndex $ do
 	g <- gitRepo
 	let dir = gitAnnexJournalDir g
-	fs <- getJournalFiles
+	fs <- getJournalFiles jl
 	liftIO $ do
 		h <- hashObjectStart g
 		Git.UpdateIndex.streamUpdateIndex g
@@ -404,10 +402,9 @@ stageJournal = withIndex $ do
  - remote refs cannot be merged into the branch (since transitions
  - throw away history), so they are added to the list of refs to ignore,
  - to avoid re-merging content from them again.
- -
- - Should be called only inside lockJournal. -}
-handleTransitions :: Transitions -> [Git.Ref] -> Annex Bool
-handleTransitions localts refs = do
+ -}
+handleTransitions :: JournalLocked -> Transitions -> [Git.Ref] -> Annex Bool
+handleTransitions jl localts refs = do
 	m <- M.fromList <$> mapM getreftransition refs
 	let remotets = M.elems m
 	if all (localts ==) remotets
@@ -416,7 +413,7 @@ handleTransitions localts refs = do
 			let allts = combineTransitions (localts:remotets)
 			let (transitionedrefs, untransitionedrefs) =
 				partition (\r -> M.lookup r m == Just allts) refs
-			performTransitionsLocked allts (localts /= allts) transitionedrefs
+			performTransitionsLocked jl allts (localts /= allts) transitionedrefs
 			ignoreRefs untransitionedrefs
 			return True
   where
@@ -444,10 +441,10 @@ getIgnoredRefs = S.fromList . mapMaybe Git.Sha.extractSha . lines <$> content
  - commits it to the branch, or creates a new branch.
  -}
 performTransitions :: Transitions -> Bool -> [Ref] -> Annex ()
-performTransitions ts neednewlocalbranch transitionedrefs = lockJournal $
-	performTransitionsLocked ts neednewlocalbranch transitionedrefs
-performTransitionsLocked :: Transitions -> Bool -> [Ref] -> Annex ()
-performTransitionsLocked ts neednewlocalbranch transitionedrefs = do
+performTransitions ts neednewlocalbranch transitionedrefs = lockJournal $ \jl ->
+	performTransitionsLocked jl ts neednewlocalbranch transitionedrefs
+performTransitionsLocked :: JournalLocked -> Transitions -> Bool -> [Ref] -> Annex ()
+performTransitionsLocked _jl ts neednewlocalbranch transitionedrefs = do
 	-- For simplicity & speed, we're going to use the Annex.Queue to
 	-- update the git-annex branch, while it usually holds changes
 	-- for the head branch. Flush any such changes.
diff --git a/Annex/Journal.hs b/Annex/Journal.hs
index fff20ccc4..8b88ab2fb 100644
--- a/Annex/Journal.hs
+++ b/Annex/Journal.hs
@@ -1,10 +1,10 @@
 {- management of the git-annex journal
  -
  - The journal is used to queue up changes before they are committed to the
- - git-annex branch. Amoung other things, it ensures that if git-annex is
+ - git-annex branch. Among other things, it ensures that if git-annex is
  - interrupted, its recorded data is not lost.
  -
- - Copyright 2011 Joey Hess <joey@kitenet.net>
+ - Copyright 2011-2013 Joey Hess <joey@kitenet.net>
  -
  - Licensed under the GNU GPL version 3 or higher.
  -}
@@ -23,9 +23,14 @@ import Annex.Perms
 {- Records content for a file in the branch to the journal.
  -
  - Using the journal, rather than immediatly staging content to the index
- - avoids git needing to rewrite the index after every change. -}
-setJournalFile :: FilePath -> String -> Annex ()
-setJournalFile file content = do
+ - avoids git needing to rewrite the index after every change.
+ - 
+ - The file in the journal is updated atomically, which allows
+ - getJournalFileStale to always return a consistent journal file
+ - content, although possibly not the most current one.
+ -}
+setJournalFile :: JournalLocked -> FilePath -> String -> Annex ()
+setJournalFile _jl file content = do
 	createAnnexDirectory =<< fromRepo gitAnnexJournalDir
 	createAnnexDirectory =<< fromRepo gitAnnexTmpDir
 	-- journal file is written atomically
@@ -37,17 +42,32 @@ setJournalFile file content = do
 		moveFile tmpfile jfile
 
 {- Gets any journalled content for a file in the branch. -}
-getJournalFile :: FilePath -> Annex (Maybe String)
-getJournalFile file = inRepo $ \g -> catchMaybeIO $
+getJournalFile :: JournalLocked -> FilePath -> Annex (Maybe String)
+getJournalFile _jl = getJournalFileStale
+
+{- Without locking, this is not guaranteed to be the most recent
+ - version of the file in the journal, so should not be used as a basis for
+ - changes. -}
+getJournalFileStale :: FilePath -> Annex (Maybe String)
+getJournalFileStale file = inRepo $ \g -> catchMaybeIO $
 	readFileStrict $ journalFile file g
 
 {- List of files that have updated content in the journal. -}
-getJournalledFiles :: Annex [FilePath]
-getJournalledFiles = map fileJournal <$> getJournalFiles
+getJournalledFiles :: JournalLocked -> Annex [FilePath]
+getJournalledFiles jl = map fileJournal <$> getJournalFiles jl
+
+getJournalledFilesStale :: Annex [FilePath]
+getJournalledFilesStale = map fileJournal <$> getJournalFilesStale
 
 {- List of existing journal files. -}
-getJournalFiles :: Annex [FilePath]
-getJournalFiles = do
+getJournalFiles :: JournalLocked -> Annex [FilePath]
+getJournalFiles _jl = getJournalFilesStale
+
+{- List of existing journal files, but without locking, may miss new ones
+ - just being added, or may have false positives if the journal is staged
+ - as it is run. -}
+getJournalFilesStale :: Annex [FilePath]
+getJournalFilesStale = do
 	g <- gitRepo
 	fs <- liftIO $ catchDefaultIO [] $
 		getDirectoryContents $ gitAnnexJournalDir g
@@ -55,7 +75,7 @@ getJournalFiles = do
 
 {- Checks if there are changes in the journal. -}
 journalDirty :: Annex Bool
-journalDirty = not . null <$> getJournalFiles
+journalDirty = not . null <$> getJournalFilesStale
 
 {- Produces a filename to use in the journal for a file on the branch.
  -
@@ -77,14 +97,19 @@ fileJournal :: FilePath -> FilePath
 fileJournal = replace [pathSeparator, pathSeparator] "_" .
 	replace "_" [pathSeparator]
 
+{- Sentinal value, only produced by lockJournal; required
+ - as a parameter by things that need to ensure the journal is
+ - locked. -}
+data JournalLocked = ProduceJournalLocked
+
 {- Runs an action that modifies the journal, using locking to avoid
  - contention with other git-annex processes. -}
-lockJournal :: Annex a -> Annex a
+lockJournal :: (JournalLocked -> Annex a) -> Annex a
 lockJournal a = do
 	lockfile <- fromRepo gitAnnexJournalLock
 	createAnnexDirectory $ takeDirectory lockfile
 	mode <- annexFileMode
-	bracketIO (lock lockfile mode) unlock (const a)
+	bracketIO (lock lockfile mode) unlock (const $ a ProduceJournalLocked)
   where
 #ifndef mingw32_HOST_OS
 	lock lockfile mode = do
@@ -101,4 +126,3 @@ lockJournal a = do
 #else
 	unlock = removeFile
 #endif
-