bluuebunny/crossref_metadata_2025 huggingface dataset:
Engineering with logic
Authors: Bishop Steve , Fairbairn Matthew , Norrish Michael , Sewell Peter , Smith Michael , Wansbrough Keith
Published: February 2006

The TCP/IP protocols and Sockets API underlie much of modern computation, but their semantics have historically been very complex and ill-defined. The real standard is the de facto one of the common implementations, including, for example, the 15,000--20,000 lines of C in the BSD implementation. Dealing rigorously with the behaviour of such bodies of code is challenging.We have recently developed a post-hoc specification of TCP, UDP, and Sockets that is rigorous, detailed, readable, has broad coverage, and is remarkably accurate. In this paper we describe the novel techniques that were required.Working within a general-purpose proof assistant (HOL), we developed
language idioms
(within higher-order logic) in which to write the specification: operational semantics with nondeterminism, time, system calls, monadic relational programming, etc. We followed an
experimental semantics
approach, validating the specification against several thousand traces captured from three implementations (FreeBSD, Linux, and WinXP). Many differences between these were identified, and a number of bugs. Validation was done using a special-purpose
symbolic model checker
programmed above HOL.We suggest that similar logic engineering techniques could be applied to future critical software infrastructure at design time, leading to cleaner designs and (via specification-based testing using a similar checker) more predictable implementations.
Decidability and proof systems for language-based noninterference relations
Authors: Dam Mads
Published: February 2006

Noninterference is the basic semantical condition used to account for confidentiality and integrity-related properties in programming languages. There appears to be an at least implicit belief in the programming languages community that partial approaches based on type systems or other static analysis techniques are necessary for noninterference analyses to be tractable. In this paper we show that this belief is not necessarily true. We focus on the notion of strong low bisimulation proposed by Sabelfeld and Sands. We show that, relative to a decidable expression theory, strong low bisimulation is decidable for a simple parallel while-language, and we give a sound and relatively complete proof system for deriving noninterference assertions. The completeness proof provides an effective proof search strategy. Moreover, we show that common alternative noninterference relations based on traces or input-output relations are undecidable. The first part of the paper is cast in terms of multi-level security. In the second part of the paper we generalize the setting to accommodate a form of intransitive interference. We discuss the model and show how the decidability and proof system results generalize to this richer setting.
On flow-sensitive security types
Authors: Hunt Sebastian , Sands David
Published: February 2006

This article investigates formal properties of a family of semantically sound flow-sensitive type systems for tracking information flow in simple While programs. The family is indexed by the choice of flow lattice.By choosing the flow lattice to be the powerset of program variables, we obtain a system which, in a very strong sense, subsumes all other systems in the family (in particular, for each program, it provides a principal typing from which all others may be inferred). This distinguished system is shown to be equivalent to, though more simply described than, Amtoft and Banerjee's Hoare-style independence logic (SAS'04).In general, some lattices are more expressive than others. Despite this, we show that no type system in the family can give better results for a given choice of lattice than the type system for that lattice itself.Finally, for any program typeable in one of these systems, we show how to construct an equivalent program which is typeable in a simple flow-insensitive system. We argue that this general approach could be useful in a proof-carrying-code setting.
A logic for information flow in object-oriented programs
Authors: Amtoft Torben , Bandhakavi Sruthi , Banerjee Anindya
Published: February 2006

This paper specifies, via a Hoare-like logic, an interprocedural and flow sensitive (but termination insensitive) information flow analysis for object-oriented programs. Pointer aliasing is ubiquitous in such programs, and can potentially leak confidential information. Thus the logic employs
independence assertions
to describe the noninterference property that formalizes confidentiality, and employs
region assertions
to describe possible aliasing. Programmer assertions, in the style of JML, are also allowed, thereby permitting a more fine-grained specification of information flow policy.The logic supports local reasoning about state in the style of separation logic. Small specifications are used; they mention only the variables and addresses relevant to a command. Specifications are combined using a frame rule. An algorithm for the computation of postconditions is described: under certain assumptions, there exists a
strongest
postcondition which the algorithm computes.
Verifying properties of well-founded linked lists
Authors: Lahiri Shuvendu K. , Qadeer Shaz
Published: February 2006

We describe a novel method for verifying programs that manipulate linked lists, based on two new predicates that characterize reachability of heap cells. These predicates allow reasoning about both acyclic and cyclic lists uniformly with equal ease. The crucial insight behind our approach is that a circular list invariably contains a
distinguished head cell
that provides a handle on the list. This observation suggests a programming methodology that requires the heap of the program at each step to be
well-founded
, i.e., for any field
f
in the program, every sequence
u
.f,
u
.f.f,
... contains at least one head cell. We believe that our methodology captures the most common idiom of programming with linked data structures. We enforce our methodology by automatically instrumenting the program with updates to two auxiliary variables representing these predicates and adding assertions in terms of these auxiliary variables.To prove program properties and the instrumented assertions, we provide a first-order axiomatization of our two predicates. We also introduce a novel induction principle made possible by the well-foundedness of the heap. We use our induction principle to derive from two basic axioms a small set of additional first-order axioms that are useful for proving the correctness of several programs.We have implemented our method in a tool and used it to verify the correctness of a variety of nontrivial programs manipulating both acyclic and cyclic singly-linked lists and doubly-linked lists. We also demonstrate the use of indexed predicate abstraction to automatically synthesize loop invariants for these examples.
Environment analysis via ΔCFA
Authors: Might Matthew , Shivers Olin
Published: February 2006

We describe a new program-analysis framework, based on CPS and procedure-string abstractions, that can handle critical analyses which the
k
-CFA framework cannot. We present the main theorems concerning correctness, show an application analysis, and describe a running implementation.
A fixpoint calculus for local and global program flows
Authors: Alur Rajeev , Chaudhuri Swarat , Madhusudan P.
Published: February 2006

We define a new fixpoint modal logic,
the visibly pushdown μ-calculus
(VP-μ), as an extension of the modal μ-calculus. The models of this logic are execution trees of structured programs where the procedure calls and returns are made visible. This new logic can express pushdown specifications on the model that its classical counterpart cannot, and is motivated by recent work on visibly pushdown languages [4]. We show that our logic naturally captures several interesting program specifications in program verification and dataflow analysis. This includes a variety of program specifications such as computing combinations of local and global program flows, pre/post conditions of procedures, security properties involving the context stack, and interprocedural dataflow analysis properties. The logic can capture flow-sensitive and inter-procedural analysis, and it has constructs that allow skipping procedure calls so that
local flows
in a procedure can also be tracked. The logic generalizes the semantics of the modal μ-calculus by considering
summaries
instead of nodes as first-class objects, with appropriate constructs for concatenating summaries, and naturally captures the way in which pushdown models are model-checked. The main result of the paper is that the model-checking problem for VP-μ is effectively solvable against pushdown models with no more effort than that required for weaker logics such as CTL. We also investigate the expressive power of the logic VP-μ: we show that it encompasses all properties expressed by a corresponding pushdown temporal logic on linear structures (
caret
[2]) as well as by the classical μ-calculus. This makes VP-μ the most expressive known program logic for which algorithmic software model checking is feasible. In fact, the decidability of most known program logics (μ-calculus, temporal logics LTL and CTL,
caret
, etc.) can be understood by their interpretation in the monadic second-order logic over trees. This is not true for the logic VP-μ, making it a new powerful tractable program logic.
Adventures in time and space
Authors: Danner Norman , Royer James S.
Published: February 2006

This paper investigates what is essentially a call-by-value version of PCF under a complexity-theoretically motivated type system. The programming formalism, ATR1, has its first-order programs characterize the poly-time computable functions, and its second-order programs characterize the type-2 basic feasible functionals of Mehlhorn and of Cook and Urquhart. (The ATR1-types are confined to levels 0, 1, and 2.) The type system comes in two parts, one that primarily restricts the sizes of values of expressions and a second that primarily restricts the time required to evaluate expressions. The size-restricted part is motivated by Bellantoni and Cook's and Leivant's implicit characterizations of poly-time. The time-restricting part is an affine version of Barber and Plotkin's DILL. Two semantics are constructed for ATR
1
. The first is a pruning of the naïve denotational semantics for ATR
1
. This pruning removes certain functions that cause otherwise feasible forms of recursion to go wrong. The second semantics is a model for ATR
1
's time complexity relative to a certain abstract machine. This model provides a setting for complexity recurrences arising from ATR1 recursions, the solutions of which yield second-order polynomial time bounds. The time-complexity semantics is also shown to be sound relative to the costs of interpretation on the abstract machine.
N
-synchronous Kahn networks
Authors: Cohen Albert , Duranton Marc , Eisenbeis Christine , Pagetti Claire , Plateau Florence , Pouzet Marc
Published: February 2006

The design of high-performance stream-processing systems is a fast growing domain, driven by markets such like high-end TV, gaming, 3D animation and medical imaging. It is also a surprisingly demanding task, with respect to the algorithmic and conceptual simplicity of streaming applications. It needs the close cooperation between numerical analysts, parallel programming experts, real-time control experts and computer architects, and incurs a very high level of quality insurance and optimization.In search for improved productivity, we propose a programming model and language dedicated to high-performance stream processing. This language builds on the synchronous programming model and on domain knowledge -- the periodic evolution of streams -- to allow correct-by-construction properties to be proven by the compiler. These properties include resource requirements and delays between input and output streams. Automating this task avoids tedious and error-prone engineering, due to the combinatorics of the composition of filters with multiple data rates and formats. Correctness of the implementation is also difficult to assess with traditional (asynchronous, simulation-based) approaches. This language is thus provided with a relaxed notion of synchronous composition, called
n-synchrony
: two processes are n-synchronous if they can communicate in the ordinary (0-)synchronous model with a FIFO buffer of size n.Technically, we extend a core synchronous data-flow language with a notion of periodic clocks, and design a relaxed clock calculus (a type system for clocks) to allow non strictly synchronous processes to be composed or correlated. This relaxation is associated with two sub-typing rules in the clock calculus. Delay, buffer insertion and control code for these buffers are automatically inferred from the clock types through a systematic transformation into a standard synchronous program. We formally define the semantics of the language and prove the soundness and completeness of its clock calculus and synchronization transformation. Finally, the language is compared with existing formalisms.
Compiler-directed channel allocation for saving power in on-chip networks
Authors: Chen Guangyu , Li Feihui , Kandemir Mahmut
Published: February 2006

Increasing complexity in the communication patterns of embedded applications parallelized over multiple processing units makes it difficult to continue using the traditional bus-based on-chip communication techniques. The main contribution of this paper is to demonstrate the importance of compiler technology in reducing power consumption of applications designed for emerging multi processor, NoC (Network-on-Chip) based embedded systems. Specifically, we propose and evaluate a compiler-directed approach to NoC power management in the context of array-intensive applications, used frequently in embedded image/video processing. The unique characteristic of the compiler-based approach proposed in this paper is that it increases the idle periods of communication channels by reusing the same set of channels for as many communication messages as possible. The unused channels in this case take better advantage of the underlying power saving mechanism employed by the network architecture. However, this channel reuse optimization should be applied with care as it can hurt performance if two or more simultaneous communications are mapped onto the same set of channels. Therefore, the problem addressed in this paper is one of reducing the number of channels used to implement a set of communications without increasing the communication latency significantly. To test the effectiveness of our approach, we implemented it within an optimizing compiler and performed experiments using twelve application codes and a network simulation environment. Our experiments show that the proposed compiler-based approach is very successful in practice and works well under both hardware based and software based channel turn-off schemes.
Modular set-based analysis from contracts
Authors: Meunier Philippe , Findler Robert Bruce , Felleisen Matthias
Published: February 2006

In PLT Scheme, programs consist of modules with contracts. The latter describe the inputs and outputs of functions and objects via predicates. A run-time system enforces these predicates; if a predicate fails, the enforcer raises an exception that blames a specific module with an explanation of the fault.In this paper, we show how to use such module contracts to turn set-based analysis into a fully modular parameterized analysis. Using this analysis, a static debugger can indicate for any given contract check whether the corresponding predicate is always satisfied, partially satisfied, or (potentially) completely violated. The static debugger can also predict the source of potential errors, i.e., it is sound with respect to the blame assignment of the contract system.
The next mainstream programming language
Authors: Sweeney Tim
Published: February 2006

Game developers have long been early adopters of new technologies. This is so because we are largely unburdened by legacy code: With each new hardware generation, we are free to rethink our software assumptions and develop new products using new tools and even new programming languages. As a result, games are fertile ground for applying academic advances in these areas.And never has our industry been in need of such advances as it is now! The scale and scope of game development has increased more than ten-fold over the past ten years, yet the underlying limitations of the mainstream C/C++/Java/C# language family remain largely unaddressed.The talk begins with a high-level presentation of the game developer's world: the kinds of algorithms we employ on modern CPUs and GPUs, the difficulties of componentization and concurrency, and the challenges of writing very complex software with real-time performance requirements.The talk then outlines the ways that future programming languages could help us write better code, providing examples derived from experience writing games and software frameworks that support games. The major areas covered are abstraction facilities -- how we can use them to develop more extensible frameworks and components; practical opportunities for employing stronger typing to reduce run-time failures; and the need for pervasive concurrency support, both implicit and explicit, to effectively exploit the several forms of parallelism present in games and graphics.
Certified assembly programming with embedded code pointers
Authors: Ni Zhaozhong , Shao Zhong
Published: February 2006

Embedded code pointers (ECPs) are stored handles of functions and continuations commonly seen in low-level binaries as well as functional or higher-order programs. ECPs are known to be very hard to support well in Hoare-logic style verification systems. As a result, existing proof-carrying code (PCC) systems have to either sacrifice the expressiveness or the modularity of program specifications, or resort to construction of complex semantic models. In Reynolds's LICS'02 paper, supporting ECPs is listed as one of the main open problems for separation logic.In this paper we present a simple and general technique for solving the ECP problem for Hoare-logic-based PCC systems. By adding a small amount of syntax to the assertion language, we show how to combine semantic consequence relation with syntactic proof techniques. The result is a new powerful framework that can perform modular reasoning on ECPs while still retaining the expressiveness of Hoare logic. We show how to use our techniques to support polymorphism, closures, and other language extensions and how to solve the ECP problem for separation logic. Our system is fully mechanized. We give its complete soundness proof and a full verification of Reynolds's CPS-style "list-append" example in the Coq proof assistant.
Associating synchronization constraints with data in an object-oriented language
Authors: Vaziri Mandana , Tip Frank , Dolby Julian
Published: February 2006

Concurrency-related bugs may happen when multiple threads access shared data and interleave in ways that do not correspond to any sequential execution. Their absence is not guaranteed by the traditional notion of "data race" freedom. We present a new definition of data races in terms of 11 problematic interleaving scenarios, and prove that it is
complete
by showing that any execution not exhibiting these scenarios is serializable for a chosen set of locations. Our definition subsumes the traditional definition of a data race as well as high-level data races such as stale-value errors and inconsistent views. We also propose a language feature called
atomic sets
of locations, which lets programmers specify the
existence
of consistency properties between fields in objects, without specifying the properties themselves. We use static analysis to
automatically infer
those points in the code where synchronization is needed to avoid data races under our new definition. An important benefit of this approach is that, in general, far fewer annotations are required than is the case with existing approaches such as synchronized blocks or atomic sections. Our implementation successfully inferred the appropriate synchronization for a significant subset of Java's Standard Collections framework.
Autolocker
Authors: McCloskey Bill , Zhou Feng , Gay David , Brewer Eric
Published: February 2006

The movement to multi-core processors increases the need for simpler, more robust parallel programming models. Atomic sections have been widely recognized for their ease of use. They are simpler and safer to use than manual locking and they increase modularity. But existing proposals have several practical problems, including high overhead and poor interaction with I/O. We present pessimistic atomic sections, a fresh approach that retains many of the advantages of optimistic atomic sections as seen in "transactional memory" without sacrificing performance or compatibility. Pessimistic atomic sections employ the locking mechanisms familiar to programmers while relieving them of most burdens of lock-based programming, including deadlocks. Significantly, pessimistic atomic sections separate correctness from performance: they allow programmers to extract more parallelism via finer-grained locking without fear of introducing bugs. We believe this property is crucial for exploiting multi-core processor designs.We describe a tool, Autolocker, that automatically converts pessimistic atomic sections into standard lock-based code. Autolocker relies extensively on program analysis to determine a correct locking policy free of deadlocks and race conditions. We evaluate the expressiveness of Autolocker by modifying a 50,000 line high-performance web server to use atomic sections while retaining the original locking policy. We analyze Autolocker's performance using microbenchmarks, where Autolocker outperforms software transactional memory by more than a factor of 3.
Protecting representation with effect encapsulation
Authors: Lu Yi , Potter John
Published: February 2006

Representation exposure is a well-known problem in the object-oriented realm. Object encapsulation mechanisms have established a tradition for solving this problem based on a principle of reference containment. This paper proposes a novel type system which is based on a different principle, we call
effect encapsulation
, which confines side effects, rather than object references, according to an ownership structure. Compared to object encapsulation, effect encapsulation liberates us from the restriction on object referenceability and offers more flexibility. In this paper, we show that effect encapsulation can be statically type checked.
The essence of command injection attacks in web applications
Authors: Su Zhendong , Wassermann Gary
Published: February 2006

Web applications typically interact with a back-end database to retrieve persistent data and then present the data to the user as dynamically generated output, such as HTML web pages. However, this interaction is commonly done through a low-level API by dynamically constructing query strings within a general-purpose programming language, such as Java. This low-level interaction is ad hoc because it does not take into account the structure of the output language. Accordingly, user inputs are treated as isolated lexical entities which, if not properly sanitized, can cause the web application to generate unintended output. This is called a
command injection attack
, which poses a serious threat to web application security. This paper presents the first formal definition of command injection attacks in the context of web applications, and gives a sound and complete algorithm for preventing them based on context-free grammars and compiler parsing techniques. Our key observation is that, for an attack to succeed, the input that gets propagated into the database query or the output document must change the intended syntactic structure of the query or document. Our definition and algorithm are general and apply to many forms of command injection attacks. We validate our approach with
SqlCheckS
, an implementation for the setting of SQL command injection attacks. We evaluated
SqlCheckS
on real-world web applications with systematically compiled real-world attack data as input.
SqlCheckS
produced no false positives or false negatives, incurred low runtime overhead, and applied straightforwardly to web applications written in different languages.
Harmless advice
Authors: Dantas Daniel S. , Walker David
Published: February 2006

This paper defines an object-oriented language with
harmless
aspect-oriented advice. A piece of harmless advice is a computation that, like ordinary aspect-oriented advice, executes when control reaches a designated control-flow point. However, unlike ordinary advice, harmless advice is designed to obey a weak non-interference property. Harmless advice may change the termination behavior of computations and use I/O, but it does not otherwise influence the final result of the mainline code. The benefit of harmless advice is that it facilitates local reasoning about program behavior. More specifically, programmers may ignore harmless advice when reasoning about the partial correctness properties of their programs. In addition, programmers may add new pieces of harmless advice to pre-existing programs in typical "after-the-fact" aspect-oriented style without fear they will break important data invariants used by the mainline code.In order to detect and enforce harmlessness, the paper defines a novel type and effect system related to information-flow type systems. The central technical result is that well-typed harmless advice does not interfere with the mainline computation. The paper also presents an implementation of the language and a case study using harmless advice to implement security policies.
Staged allocation
Authors: Olinsky Reuben , Lindig Christian , Ramsey Norman
Published: February 2006

We present
staged allocation
, a technique for specifying calling conventions by composing tiny allocators called
stages
. A specification written using staged allocation has a precise, formal semantics, and it can be executed directly inside a compiler. Specifications of nine standard C~calling conventions range in size from 15 to 30 lines each. An implementation of staged allocation takes about 250 lines of ML or 650~lines of C++. Each specification can be used not only to help a compiler implement the calling convention but also to generate a test suite.
Public review for secure distributed dataMining and its application largescale network measurements
Authors: Crovella Mark
Published: February 2006

This paper considers a problem that plagues both Internet research and operation: obtaining global statistical meas-ures that span the domains of multiple ISPs. ISPs generally consider many important performance measures of their networks to be competition sensitive. How then to gauge the size of the Internet, or measure the amount of traffic it is carrying, detect the presence of Internet-wide anomalies or other phenomena, or perform many other similar measurements?This paper makes a good case for the need to collect a variety of global statistics of Internet size and performance. It then points out that the problem may in principle be solvable: research in cyptography has developed methods for multiparty computations in which no single party actually reveals its own contribution to the other parties involved. Reviewers liked the problem definition and the general approach. It is clear that the work in this paper is still in the early stages, but this is to be expected. The most pointed reviewer comments concerned the cryptographic methods employed in the paper. The problem considered is a special case of secure multiparty computation, which has been considered in cryptography for over 20 years, starting with work by Yao in 1982 and Goldreich, Micali and Widgerson in 1987. The method proposed in this paper is one of many that could be employed; alternatives can be found by consulting the cryptography literature. On the positive side, the paper considers the kind of implementation details that are not usually considered in the cryptography literatureIn summary, this paper should stimulate more research into the problem of collecting certain kinds of Internet-wide measurements. Researchers have commonly assumed these kinds of measurements to be essentially impossible to obtain for practical reasons. Maybe not!
Public review for the internet AS-level topology
Authors: Faloutsos Michalis
Published: February 2006

The paper provides an overview of the current available data sets for AS level topology and examines the usefulness and intuition of many and most widely used metrics used for graph analysis, and highlight some less known metrics. The paper makes two practical contributions.First, the paper highlights an important issue: all source of AS information are not the same. The paper utilizes three sources of information BGP tables, traceroute-based and archived information (WHOIS/IRR). The observed topo-logical properties are fairly different. A potential explanation could be that none of the sources captures the whole AS graph. Thus, the measurement community has more work to do to obtain a complete topology.Second, the paper critically analyzes the importance of the different topology metrics. The last six years have seen a proliferation of new metrics that are used in a selective fashion from researchers. This is one of the first thorough studies of most known metrics and on top of that many metrics that are used in related fields that also study networks (e.g. physics).In conclusion, this paper could become a reference point for making the analysis of the AS topology more systematic both in terms of making researchers: (a) aware of the differences among the datasets, and (b) careful in selecting metrics.
Public review for the devil and packet trace anonymization
Authors: Roughan Matt
Published: February 2006

Reproducible research hinges on the ability to use common datasets, and so public datasets containing measurements of real, operational networks are important for the Internet measurement community, and subsequently for all those fields of networking that use their research. There are several such datasets available now, but given the ongoing evolution of the Internet, more are always needed. However, such data is often considered proprietary, or its release raises privacy or security concerns, and so access to data is often limited to the organization that collected itAnonymization of data has sometimes been used to remove the offending components of a dataset so that the remainder can be made public.As with all such work, the Devil is in the detail. Different organizations have their own requirements for anonymization, while on the other hand, researchers have different interests in a dataset. Particular aspects of an anonymization may remove the component of the data that is of interest in a study. Anonymization policies that balance security and privacy with research value are needed. It is a challenging problem --- as one reviewer put it "the difference between a researcher and an attacker cannot be expressed in pure data analysis terms. It is motivation or funding source that makes the difference.In studying the issues of their own organization, the authors of this paper sought not to add a new tool that would perform anonymization according to their own policies, but rather they aimed to create a new (freely available) tool 'tcpmkpub,' which would allow one to implement complicated, multifaceted anonymization policies, considerably beyond the capabilities of existing tools. The paper also provides considerable discussion of the issues surrounding anonymization policies, and finally provides access to a large dataset (11 GB set of packet traces anonymized using their tool)The reviewers were all largely positive about the paper, for instance saying "it raises the level of thoroughness at which packet traces are anonymized," and "The authors present a tool able to fulfil this task [anonymization] in an elegant way and whose flexibility promises to make it easy to adapt in different environments." However, two reviewers noted the fundamental problem of making a trace totally attacker proof is not solved here, though this problem is highly challenging, and perhaps not solvable --- so there is plenty of remaining research to be performed in this area
Public review for LTCP
Authors: Katabi Dina
Published: February 2006

LTCP is a new modification to TCP's congestion control to enable it to scale to high-speed networks. In comparison with prior work on high-speed congestion control, the paper explores an interesting design space: what if a single flow acts similarly to K virtual TCPs, where K is dynamically adjusted according to the network's congestion state; K increases in times of under-load to aggressively grab the available bandwidth and decreases in times of congestion to quickly release the bandwidth. The paper elaborates on how to design such a protocol and particularly how to make it fair when multiple flows with a different initial K share the same bottleneckThough I find it interesting to explore such a design, with much prior work on high-speed congestion control, it is unclear what LTCP can add. The paper claims that one of the contributions of LTCP is that "it retains the time-tested AIMD behavior of TCP." Yet, because of the dynamic value of K, LTCP does not really do AIMD. Besides, why is maintaining AIMD important? The paper does not elaborate on this issue; neither does it show that the use of different increase-decrease rule has hurt other high-speed congestion control protocolsOverall, LTCP is a nice piece of research but I would encourage the authors to argue more why their design is important given all prior work on the topic. Further, they should run more extensive simulations that explore multiple bottleneck links, and provide at least a simple analysis that supports the convergence claim.
Network coding
Authors: Fragouli Christina , Le Boudec Jean-Yves , Widmer Jörg
Published: February 2006

Network coding is a new research area that may have interesting applications in practical networking systems. With network coding, intermediate nodes may send out packets that are linear combinations of previously received information. There are two main benefits of this approach: potential throughput improvements and a high degree of robustness. Robustness translates into loss resilience and facilitates the design of simple distributed algorithms that perform well, even if decisions are based only on partial information. This paper is an instant primer on network coding: we explain what network coding does and how it does it. We also discuss the implications of theoretical results on network coding for realistic settings and show how network coding can be used in practice
Efficient and decentralized computation of approximate global state
Authors: Keshav S.
Published: February 2006

The need for efficient computation of approximate global state lies at the heart of a wide range of problems in distributed systems. Examples include routing in the Internet, sensor fusion, search in peer-to-peer networks, coordinated intrusion detection, and Top-K queries in stream-oriented databases. Efficient algorithms that determine approximate global state could enable near-optimal local decision-making with little overhead. In this position paper, we model this problem and summarize recent work on randomized algorithms that navigate a four-way tradeo between accuracy, robustness, performance and overhead. Despite these recent successes, many open problems remain. We believe that solving these problems can radically improve the design of robust, efficient and self-managed distributed systems
On the feasibility of commercial, legal P2P content distribution
Authors: Rodriguez Pablo , Tan See-Mong , Gkantsidis Christos
Published: February 2006

A spirited panel was recently held at the 10th International Web Caching and Content Distribution workshop on the future of P2P in content distribution [1]. After more than ten years of content distribution research and technology efforts, P2P is emerging as an alternative solution to solve the mass distribution of large digital content. However, using P2P for commercial content distribution faces a number of serious challenges. Issues such as content protection, impact on ISPs, security, end-to-end connectivity, and business models need careful consideration before P2P an be used as an efficient tool by content providers. In this paper, we summarize the issues brought up in discussion, and delve deeper into the feasibility of commercial, legal P2P content distribution solutions
Counting 6to4 relay routers
Authors: Malone David
Published: February 2006

6to4 is a mechanism or providing IPv6 addresses and connectivity where native IPv6 is not available. In 6to4, the links between the IPv4 and IPv6 Internets are called
relay routers
These may be advertised publicly or privately. The number of 6to4 relay routers has been the subject of debate, as additional routers increase the scalability and efficency of the 6to4 system. Counting public relay routers is easy using the global routing table. This paper outlines a technique that can count private relay routers and reports results of applying this method. Our results indicate that there are a significant number of private relays in operation in comparison to the number of public relays. This number has increased over the last two years. The results also indicate that using distributed traceroute facilities to measure the multiplicity of an anycast deployment requires large numbers of nodes to be accurate
Open issues in router buffer sizing
Authors: Dhamdhere Amogh , Dovrolis Constantine
Published: February 2006

Recent research results suggest that the buffers of router interfaces can be made very small, much less than the link's and width-delay product, without causing a utilization loss, as long as the link carries many TCP flows. In this letter we raise some concerns about the previous recommendation. We show that the use of such small buffers can lead to excessively high loss rates (up to 5%-15%in our simulations) in congested access links that carry many flows. Even if the link is fully utilized, small buffers lead to lower throughput for most large TCP flows, and significant variability in the per-flow throughput and transfer latency. We also discuss some important issues in router buffer sizing that are often ignored
Fairness, QoS, and buffer sizing
Authors: Wischik Damon
Published: February 2006

This note is a reply to some of the points about buffer sizing raised by Dhamdhere and Dovrolis [1]. I'll use a simple mathematical model to make stark some of the tradeoffs that need to be weighed when deciding on buffer size.
An on-the-fly reference-counting garbage collector for java
Authors: Levanoni Yossi , Petrank Erez
Published: February 2006

Reference-counting is traditionally considered unsuitable for multiprocessor systems. According to conventional wisdom, the update of reference slots and reference-counts requires atomic or synchronized operations. In this work we demonstrate this is not the case by presenting a novel reference-counting algorithm suitable for a multiprocessor system that does not require any synchronized operation in its write barrier (not even a compare-and-swap type of synchronization). A second novelty of this algorithm is that it allows eliminating a large fraction of the reference-count updates, thus, drastically reducing the reference-counting traditional overhead. This article includes a full proof of the algorithm showing that it is safe (does not reclaim live objects) and live (eventually reclaims all unreachable objects).We have implemented our algorithm on Sun Microsystems' Java Virtual Machine (JVM) 1.2.2 and ran it on a four-way IBM Netfinity 8500R server with 550-MHz Intel Pentium III Xeon and 2 GB of physical memory. Our results show that the algorithm has an extremely low latency and throughput that is comparable to the stop-the-world mark and sweep algorithm used in the original JVM.
EDO
Authors: Ogasawara Takeshi , Komatsu Hideaki , Nakatani Toshio
Published: February 2006

Optimizing exception handling is critical for programs that frequently throw exceptions. We observed that there are many such exception-intensive programs written in Java. There are two commonly used exception handling techniques, stack unwinding and stack cutting. Stack unwinding optimizes the normal path by leaving the exception handling path unoptimized, while stack cutting optimizes the exception handling path by adding extra work to the normal path. However, there has been no single exception handling technique to optimize the exception handling path without incurring any overhead to the normal path.We propose a new technique calledException-Directed Optimization(EDO) that optimizes exception-intensive programs without slowing down exception-minimal programs. It is a feedback-directed dynamic optimization consisting of three steps: exception path profiling, exception path inlining, and throw elimination. Exception path profiling attempts to detecthotexception paths. Exception path inlining embeds every hot exception path into the corresponding catching method. Throw elimination replaces a throw with a branch to the corresponding handler. We implemented EDO in IBM's production Just-in-Time compiler and made several experiments. In summary, it improved the performance of exception-intensive programs by up to 18.3% without decreasing the performance of exception-minimal programs for SPECjvm98. We also found an opportunity for performance improvement using EDO in the startup of a Java application server.
Effective sign extension elimination for java
Authors: Kawahito Motohiro , Komatsu Hideaki , Nakatani Toshio
Published: February 2006

Computer designs are shifting from 32-bit architectures to 64-bit architectures, while most of the programs available today are still designed for 32-bit architectures. Java, for example, specifies the frequently used “int” as a 32-bit signed integer. If such Java programs are executed on a 64-bit architecture, many 32-bit signed integers must be sign-extended to 64-bit signed integers for correct operations. This causes serious performance overhead. In this article, we present a fast and effective algorithm for eliminating sign extensions. We implemented this algorithm in the IBM Java Just-in-Time (JIT) compiler for IA-64. Our experimental results show that our algorithm effectively eliminates the majority of sign extensions. They also show that it improves performance by 6.9% for jBYTEmark and 3.3% for SPECjvm98 over the previously known best algorithm, while it increases JIT compilation time by only 0.11%.
Computability classes for enforcement mechanisms
Authors: Hamlen Kevin W. , Morrisett Greg , Schneider Fred B.
Published: February 2006

A precise characterization of those security policies enforceable by program rewriting is given. This also exposes and rectifies problems in prior work, yielding a better characterization of those security policies enforceable by execution monitors as well as a taxonomy of enforceable security policies. Some but not all classes can be identified with known classes from computational complexity theory.
Efficient management for large-scale flash-memory storage systems with resource conservation
Authors: Chang Li-Pin , Kuo Tei-Wei
Published: February 2006

Many existing approaches on flash-memory management are based on RAM-resident tables in which one single granularity size is used for both address translation and space management. As high-capacity flash memory is becoming more affordable than ever, the dilemma of how to manage the RAM space or how to improve the access performance is emerging for many vendors. In this article, we propose a tree-based management scheme which adopts multiple granularities in flash-memory management. Our objective is to not only reduce the run-time RAM footprint but also manage the write workload, due to housekeeping. The proposed method was evaluated under realistic workloads, where significant advantages over existing approaches were observed, in terms of the RAM space, access performance, and flash-memory lifetime.
Scalable and fault-tolerant support for variable bit-rate data in the exedra streaming server
Authors: Anastasiadis Stergios V. , Sevcik Kenneth C. , Stumm Michael
Published: February 2006

We describe the design and implementation of the Exedra continuous media server, and experimentally evaluate alternative resource management policies using a prototype system that we built. Exedra has been designed to provide scalable and efficient support for variable bit-rate media streams whose compression efficiency leads to reduced storage space and bandwidth requirements in comparison to constant bit-rate streams of equivalent quality. We examine alternative disk striping policies, and quantify the benefits of innovative techniques for storage space allocation, buffer management, and resource reservation, which we developed to achieve both predictability and high-performance in handling disk and network data transfers of variable size. Additionally, we investigate the differences between diverse data replication schemes over disk arrays, and compare methods for disk access time reservation that enable tolerance of disk failures at minimal cost. Overall, we demonstrate the feasibility of building network media servers that exploit the latest advances in media compression technology towards reducing the cost of wide-scale streaming services for stored data.
Triage
Authors: Karlsson Magnus , Karamanolis Christos , Zhu Xiaoyun
Published: February 2006

Ensuring performance isolation and differentiation among workloads that share a storage infrastructure is a basic requirement in consolidated data centers. Existing management tools rely on resource provisioning to meet performance goals; they require detailed knowledge of the system characteristics and the workloads. Provisioning is inherently slow to react to system and workload dynamics and, in the general case, it is not practical to provision for the worst case.We propose a software-only solution that ensures predictable performance for storage access. It is applicable to a wide range of storage systems and makes no assumptions about workload characteristics. We use an online feedback loop with an adaptive controller that throttles storage access requests to ensure that the available system throughput is shared among workloads according to their performance goals and their relative importance. The controller considers the system as a “black box” and adapts automatically to system and workload changes. The controller is distributed to ensure high availability under overload conditions, and it can be used for both block and file access protocols. The evaluation of
Triage
, our experimental prototype, demonstrates workload isolation and differentiation in an overloaded cluster file-system where workloads and system components are changing.
Characteristics of streaming media stored on the Web
Authors: Li Mingzhe , Claypool Mark , Kinicki Robert , Nichols James
Published: February 2006

Despite the growth in multimedia, there have been few studies that focus on characterizing streaming audio and video stored on the Web. This investigation used a customized Web crawler to traverse 17 million Web pages from diverse geographic locations and identify nearly 30,000 streaming audio and video clips available for analysis. Using custom-built extraction tools, these streaming media objects were analyzed to determine attributes such as media type, encoding format, playout duration, bitrate, resolution, and codec. The streaming media content encountered is dominated by proprietary audio and video formats with the top four commercial products being RealPlayer, Windows Media Player, MP3 and QuickTime. The distribution of the stored playout durations of streaming audio and video clips are long-tailed. More than half of the streaming media clips encountered are video, encoded primarily for broadband connections and at resolutions considerably smaller than the resolutions of typical monitors.