phat icon indicating copy to clipboard operation
phat copied to clipboard

check for cycles

Open agarwal opened this issue 10 years ago • 6 comments

Symbolic links lead to the possibility of cycles. Cycles are not necessarily wrong, so we don't consider them ill-formed at construction time. However, some operations will lead to an infinite loop, so we need to check for them in:

  • [ ] resolve_links
  • [ ] the proposed reify function
  • [ ] maybe in normalize also??

agarwal avatar Apr 10 '15 21:04 agarwal

Indeed not all loops are a problem. If we view a one-step resolution of a path (choose a link, and replace it by its target) as a rewriting, then we have a problem with paths such that there is no finite sequence of rewritings that leads to a link-free path. In 8f1749f we detect such cases at link creation and define them as broken links. Note that the detection is easy because all rewriting sequences are confluent.

As a result, resolve is now cycle-safe (normalize was safe to begin with because we don't normalize the target of a link), as well as typ_of and equal.

As for reify and fold, that's a different story since we have to "discover" a path and build it incrementally.

pveber avatar Nov 11 '15 16:11 pveber

Can you give examples of links that are supposed to be ruled out by 8f1749f1db2ab48685cd83e612ffed5afff81f93. I considered that x in the following two cases might be, but both return ``Ok`.

utop # let x = Item.link (name_exn "foo") (Item (Item.file (name_exn "foo")));;
val x : [ `Broken of (rel, link) item | `Ok of (rel, file) item ] =
  `Ok (Link ("foo", Item (File "foo")))
utop # let l =
  match Item.link (name_exn "foo") (Item (Item.file (name_exn "bar"))) with
  | `Broken _ -> assert false
  | `Ok x -> x;;
val l : (rel, file) item = Link ("foo", Item (File "bar"))

utop # let x = Item.link (name_exn "foo") (Item l);;
val x : [ `Broken of (rel, link) item | `Ok of (rel, file) item ] =                             
  `Ok (Link ("foo", Item (Link ("foo", Item (File "bar")))))

agarwal avatar Nov 12 '15 17:11 agarwal

These examples are not cyclic but certainly wrong since they imply the existence of two different objects with the same path. However I think this verification is more on of the filesystem duty, isn't it? At the very least in both cases you can eventually resolve the links to a file, the only problem is that you can't build a tree directory with those paths.

What I mean by cyclic in this issue really boils down to cyclic ocaml values.

pveber avatar Nov 13 '15 14:11 pveber

See the commit above, saying:

we adopt the simple (and more common) design where paths which are cyclic ocaml values are not supported and not checked. In particular, some functions may not terminate when called with such values.

This answers issue #4, which dealt with possible non termination of functions of the pure library: all legal paths are acyclic ocaml values, and as our functions on Path.t values in the pure library simply traverse them, there is no risk of infinite loop, hence no particular precaution to take.

Note that there is no danger of non-termination when dealing with the file system either:

  • either the functions in async-unix do their job by traversing a Path.t value, which guarantees termination
  • either they can discover symbolic links whose resolution run an infinite computation by just asking the filesystem, which considers such links as ill-defined and marks them as broken.

pveber avatar Dec 04 '15 21:12 pveber

IIUC correctly, you are saying we entirely can do away with our own logic for testing for cycles, except indirectly by outsourcing the work to a system call that figures it out for us. Can you confirm. If so, I can close this issue.

agarwal avatar Dec 10 '15 19:12 agarwal

Comment from 1d80c25:

"By merging this branch, we have implementations for [reify] and [fold] that can cope with cycles. The first one does so by counting on the file system to detect cases where a step-by-step discovery of link targets would loop forever; the second one uses [reify] and a set of visited nodes to avoid infinite loops."

pveber avatar Dec 15 '15 20:12 pveber