Entry Reps:2000:UCS from toplas.bib

Last update: Tue May 1 02:05:46 MDT 2012                Valid HTML 3.2!

Index sections

Top | Symbols | Math | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

BibTeX entry

@Article{Reps:2000:UCS,
  author =       "Thomas Reps",
  title =        "Undecidability of context-sensitive data-independence
                 analysis",
  journal =      j-TOPLAS,
  volume =       "22",
  number =       "1",
  pages =        "162--186",
  month =        jan,
  year =         "2000",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925 (print), 1558-4593 (electronic)",
  ISSN-L =       "0164-0925",
  bibdate =      "Tue Sep 26 10:12:58 MDT 2000",
  bibsource =    "http://www.acm.org/pubs/contents/journals/toplas/;
                 http://www.math.utah.edu/pub/tex/bib/toplas.bib",
  URL =          "http://www.acm.org/pubs/citations/journals/toplas/2000-22-1/p162-reps/",
  abstract =     "A number of program-analysis problems can be tackled
                 by transforming them into certain kinds of
                 graph-reachability problems in labeled graphs. The edge
                 labels can be used to filter out paths that are not
                 interest: a path $P$ from vertex $t$ only counts as a
                 ``valid connection'' between $s$ and $t$ if the word
                 spelled out by $P$ is in a certain language. Often the
                 languages used for such filtering purposes are
                 languages of matching parentheses. In some cases, the
                 matched-parenthesis condition is used for paths with
                 mismatched calls and returns. This leads to so-called
                 ``context-{\em sensitive\/}'' program analyses, such as
                 context-{\em sensitive\/} interprocedural slicing and
                 context-{\em sensitive\/} interprocedural dataflow
                 analysis. In other cases, the matched-parenthesis
                 condition is used to capture a graph-theoretic analog
                 of McCarthy's rules: ``car (cons(x,y)) = x'' and
                 ``cdr(cons(x,y)) =y''. That is, in the code
                 fragment\par

                 c = cons(a,b); d = car(c);\par

                 \noindent the fact that there is a
                 ``structure-transmitted data-dependence'' from a to d,
                 but not from b to d, is captured in a graph by (1)
                 using a vertex for each variable, (2) an edge from
                 vertex $i$ to vertex $j$ when $i$ is used on the
                 right-hand side of an assignment to {\em j}, (3)
                 parentheses that match as the labels on the edges that
                 run from a to c and c to d, and (4) parentheses that do
                 not match as the labels on the edges that run from a to
                 c and c to d. However, structure-transmitted
                 data-independence analysis is context-{\em
                 insensitive}, because there are no constraints that
                 these two kinds of uses of parentheses can be combined
                 to create a context-{\em sensitive\/} analysis for
                 structure-transmitted data-dependences. This article
                 answers the question in the negative: in general, the
                 problem of context {\em sensitive},
                 structure-transmitted data-dependence analysis is
                 undecidable. The results imply that in general, both
                 context-{\em sensitive\/} set-based analysis and -CFA
                 (when data constructors and selectors and selectors are
                 taken into account) are also undecidable.",
  acknowledgement = ack-nhfb,
  fjournal =     "ACM Transactions on Programming Languages and
                 Systems",
  subject =      "Software --- Programming Languages --- Processors
                 (D.3.4): {\bf Compilers}; Software --- Programming
                 Languages --- Processors (D.3.4): {\bf Optimization};
                 Theory of Computation --- Mathematical Logic and Formal
                 Languages --- Mathematical Logic (F.4.1): {\bf
                 Computability theory}; Theory of Computation ---
                 Mathematical Logic and Formal Languages --- Formal
                 Languages (F.4.3): {\bf Decision problems}; Mathematics
                 of Computing --- Discrete Mathematics --- Graph Theory
                 (G.2.2): {\bf Path and circuit problems}",
}

Related entries