bluuebunny/crossref_metadata_2025 huggingface dataset:
A complete, co-inductive syntactic theory of sequential control and state
Authors: Støvring Kristian , Lassen Soren B.
Published: April 2007

We present a new co-inductive syntactic theory,
eager normal form bisimilarity
, for the untyped call-by-value lambda calculus extended with continuations and mutable references.We demonstrate that the associated bisimulation proof principle is easy to use and that it is a powerful tool for proving equivalences between recursive imperative higher-order programs.The theory is modular in the sense that eager normal form bisimilarity for each of the calculi extended with continuations and/or mutable references is a fully abstract extension of eager normal form bisimilarity for its sub-calculi. For each calculus, we prove that eager normal form bisimilarity is a congruence and is sound with respect to contextual equivalence. Furthermore, for the calculus with both continuations and mutable references, we show that eager normal form bisimilarity is complete: it coincides with contextual equivalence.
Logic-flow analysis of higher-order programs
Authors: Might Matthew
Published: April 2007

This work presents a framework for fusing flow analysis and theorem proving called
logic-flow analysis
(LFA). The framework itself is the reduced product of two abstract interpretations: (1) an abstract state machine and (2) a set of propositions in a restricted first-order logic. The motivating application for LFA is the safe removal of implicit array-bounds checks without type information, user interaction or program annotation. LFA achieves this by delegating a given task to either the prover or the flow analysis depending on which is best suited to discharge it. Described within are a concrete semantics for continuation-passing style; a restricted, first-order logic; a woven product of two abstract interpretations; proofs of correctness; and a worked example.
Variance analyses from invariance analyses
Authors: Berdine Josh , Chawdhary Aziem , Cook Byron , Distefano Dino , O'Hearn Peter
Published: April 2007

An invariance assertion for a program location
l
is a statement that always holds at
l
during execution of the program. Program invariance analyses infer invariance assertions that can be useful when trying to prove safety properties. We use the term
variance assertion
to mean a statement that holds between any state at
l
and any previous state that was also at
l
. This paper is concerned with the development of analyses for variance assertions and their application to proving termination and liveness properties. We describe a method of constructing program variance analyses from invariance analyses. If we change the underlying invariance analysis, we get a different variance analysis. We describe several applications of the method, including variance analyses using linear arithmetic and shape analysis. Using experimental results we demonstrate that these variance analyses give rise to a new breed of termination provers which are competitive with and sometimes better than today's state-of-the-art termination provers.
Secure implementations of typed channel abstractions
Authors: Bugliesi Michele , Giunti Marco
Published: April 2007

The challenges hidden in the implementation of high-level process calculi into low-level environments are well understood [3]. This paper develops a secure implementation of a typed pi calculus, in which capability types are employed to realize the policies for the access to communication channels. Our implementation compiles high-level processes of the pi-calculus into low-level principals of a cryptographic process calculus based on the applied-pi calculus [1]. In this translation, the high-level type capabilities are implemented as term capabilities protected by encryption keys only known to the intended receivers. As such, the implementation is effective even when the compiled, low-level principals are deployed in open contexts for which no assumption on trust and behavior may be made. Our technique and results draw on, and extend, previous work on secure implementation of channel abstractions in a dialect of the join calculus [2]. In particular, our translation preserves the forward secrecy of communications in a calculus that includes matching and supports the dynamic exchange of write
and
read access-rights among processes. We establish the adequacy and full abstraction of the implementation by contrasting the untyped equivalences of the low-level cryptographic calculus, with the typed equivalences of the high-level source calculus.
Conditional must not aliasing for static race detection
Authors: Naik Mayur , Aiken Alex
Published: April 2007

Race detection algorithms for multi-threaded programs using the common lock-based synchronization idiom must correlate locks with the memory locations they guard. The heart of a proof of race freedom is showing that if two locks are distinct, then the memory locations they guard are also distinct. This is an example of a general property we call
conditional must not aliasing
: Under the assumption that two objects are not aliased, prove that two other objects are not aliased. This paper introduces and gives an algorithm for conditional must not alias analysis and discusses experimental results for sound race detection of Java programs.
Interprocedural analysis of asynchronous programs
Authors: Jhala Ranjit , Majumdar Rupak
Published: April 2007

An
asynchronous program
is one that contains procedure calls which are not immediately executed from the callsite, but stored and "dispatched" in a non-deterministic order by an external scheduler at a later point. We formalize the problem of interprocedural dataflow analysis for asynchronous programs as AIFDS problems, a generalization of the IFDS problems for interprocedural dataflow analysis. We give an algorithm for computing the precise meet-over-valid-paths solution for any AIFDS instance, as well as a
demand-driven
algorithm for solving the corresponding demand AIFDS instances. Our algorithm can be easily implemented on top of any existing interprocedural dataflow analysis framework. We have implemented the algorithm on top of B
LAST
, thereby obtaining the first safety verification tool for unbounded asynchronous programs. Though the problem of solving AIFDS instances is EXPSPACE-hard, we find that in practice our technique can efficiently analyze programs by exploiting standard optimizations of interprocedural dataflow analyses.
Preferential path profiling
Authors: Vaswani Kapil , Nori Aditya V. , Chilimbi Trishul M.
Published: April 2007

Path profiles provide a more accurate characterization of a program's dynamic behavior than basic block or edge profiles, but are relatively more expensive to collect. This has limited their use in practice despite demonstrations of their advantages over edge profiles for a wide variety of applications.We present a new algorithm called preferential path profiling (PPP), that reduces the overhead of path profiling. PPP leverages the observation that most consumers of path profiles are only interested in a subset of all program paths. PPP achieves low overhead by separating interesting paths from other paths and assigning a set of unique and compact numbers to these interesting paths. We draw a parallel between arithmetic coding and path numbering, and use this connection to prove an optimality result for the compactness of path numbering produced by PPP. This compact path numbering enables our PPP implementation to record path information in an array instead of a hash table. Our experimental results indicate that PPP reduces the runtime overhead of profiling paths exercised by the largest (ref) inputs of the SPEC CPU2000 benchmarks from 50% on average (maximum of 132%) to 15% on average (maximum of 26%) as compared to a state-of-the-art path profiler.
Multimedia simplification for optimized MMS synthesis
Authors: Yan Wei-Qi , Kankanhalli Mohan S.
Published: April 2007

We propose a novel transcoding technique called
multimedia simplification
which is based on experiential sampling. Multimedia simplification helps optimize the synthesis of MMS (multimedia messaging service) messages for mobile phones. Transcoding is useful in overcoming the limitations of these compact devices. The proposed approach aims at reducing the redundancy in the multimedia data captured by multiple types of media sensors. The simplified data is first stored into a gallery for further usage. Once a request for MMS is received, the MMS server makes use of the simplified media from the gallery. The multimedia data is aligned with respect to the timeline for MMS message synthesis. We demonstrate the use of the proposed techniques for two applications, namely, soccer video and home care monitoring video. The MMS sent to the receiver can basically reflect the gist of important events of interest to the user. Our technique is targeted towards users who are interested in obtaining salient multimedia information via mobile devices.
Detecting social interactions of the elderly in a nursing home environment
Authors: Chen Datong , Yang Jie , Malkin Robert , Wactlar Howard D.
Published: April 2007

Social interaction plays an important role in our daily lives. It is one of the most important indicators of physical or mental changes in aging patients. In this article, we investigate the problem of detecting social interaction patterns of patients in a skilled nursing facility using audio/visual records. Our studies consist of both a “Wizard of Oz” style study and an experimental study of various sensors and detection models for detecting and summarizing social interactions among aging patients and caregivers. We first simulate plausible sensors using human labeling on top of audio and visual data collected from a skilled nursing facility. The most useful sensors and robust detection models are determined using the simulated sensors. We then present the implementation of some real sensors based on video and audio analysis techniques and evaluate the performance of these implementations in detecting interactions. We conclude the article with discussions and future work.
A general approach to online network optimization problems
Authors: Alon Noga , Awerbuch Baruch , Azar Yossi , Buchbinder Niv , Naor Joseph (Seffi)
Published: April 2007

We study a wide range of online graph and network optimization problems, focusing on problems that arise in the study of connectivity and cuts in graphs. In a general online network design problem, we have a communication network known to the algorithm in advance. What is not known in advance are the connectivity (bandwidth) or cut demands between vertices in the network which arrive online.We develop a unified framework for designing online algorithms for problems involving connectivity and cuts. We first present a general
O
(log
m
)-competitive deterministic algorithm for generating a fractional solution that satisfies the online connectivity or cut demands, where
m
is the number of edges in the graph. This may be of independent interest for solving fractional online bandwidth allocation problems, and is applicable to both directed and undirected graphs. We then show how to obtain integral solutions via an online rounding of the fractional solution. This part of the framework is problem dependent, and applies various tools including results on approximate max-flow min-cut for multicommodity flow, the Hierarchically Separated Trees (HST) method and its extensions, certain rounding techniques for dependent variables, and Räcke's new hierarchical decomposition of graphs.Specifically, our results for the integral case include an
O
(log
m
log
n
)-competitive randomized algorithm for the online nonmetric facility location problem and for a generalization of the problem called the multicast problem. In the nonmetric facility location problem,
m
is the number of facilities and
n
is the number of clients. The competitive ratio is nearly tight. We also present an
O
(log
2
n
log
k
)-competitive randomized algorithm for the online group Steiner problem in trees and an
O
(log
3
n
log
k
)-competitive randomized algorithm for the problem in general graphs, where
n
is the number of vertices in the graph and
k
is the number of groups. Finally, we design a deterministic
O
(log
3
n
log log
n
)-competitive algorithm for the online multi-cut problem.
Defining user perception of distributed multimedia quality
Authors: Gulliver Stephen R. , Ghinea Gheorghita
Published: April 2007

This article presents the results of a study that explored the human side of the multimedia experience. We propose a model that assesses quality variation from three distinct levels: the network, the media and the contentlevels; and from two views: the technical and the user perspective. By facilitating parameter variation at each of the quality levels and from each of the perspectives, we were able to examine their impact on user quality perception. Results show that a significant reduction in frame rate does not proportionally reduce the user's understanding of the presentation independent of technical parameters, that multimedia content type significantly impacts user information assimilation, user level of enjoyment, and user perception of quality, and that the device display type impacts user information assimilation and user perception of quality. Finally, to ensure the transfer of information, low-level abstraction (network-level) parameters, such as delay and jitter, should be adapted; to maintain the user's level of enjoyment, high-level abstraction quality parameters (content-level), such as the appropriate use of display screens, should be adapted.
Polynomial-time quantum algorithms for Pell's equation and the principal ideal problem
Authors: Hallgren Sean
Published: April 2007

We give polynomial-time quantum algorithms for three problems from computational algebraic number theory. The first is Pell's equation. Given a positive nonsquare integer
d
, Pell's equation is
x
2
−
dy
2
= 1 and the goal is to find its integer solutions. Factoring integers reduces to finding integer solutions of Pell's equation, but a reduction in the other direction is not known and appears more difficult. The second problem we solve is the principal ideal problem in real quadratic number fields. This problem, which is at least as hard as solving Pell's equation, is the one-way function underlying the Buchmann--Williams key exchange system, which is therefore broken by our quantum algorithm. Finally, assuming the generalized Riemann hypothesis, this algorithm can be used to compute the class group of a real quadratic number field.
Robust and reliable defect control for Runge-Kutta methods
Authors: Enright W. H. , Hayes Wayne B.
Published: April 2007

The quest for reliable integration of
initial value problems
(IVPs) for
ordinary differential equations
(ODEs) is a long-standing problem in numerical analysis. At one end of the reliability spectrum are fixed stepsize methods implemented using standard floating point, where the onus lies entirely with the user to ensure the stepsize chosen is adequate for the desired accuracy. At the other end of the reliability spectrum are rigorous interval-based methods, that can provide provably correct bounds on the error of a numerical solution. This rigour comes at a price, however: interval methods are generally two to three orders of magnitude more expensive than fixed stepsize floating-point methods. Along the spectrum between these two extremes lie various methods of different expense that estimate and control some measure of the local errors and adjust the stepsize accordingly.

In this article, we continue previous investigations into a class of interpolants for use in Runge-Kutta methods that have a defect function whose qualitative behavior is asymptotically independent of the problem being integrated. In particular the point, in a step, where the maximum defect occurs as
h
→ 0 is known a priori. This property allows the defect to be monitored and controlled in an efficient and robust manner even for modestly large stepsizes. Our interpolants also have a defect with the highest possible order given the constraints imposed by the order of the underlying discrete formula. We demonstrate the approach on three Runge-Kutta methods of orders 5, 6, and 8, and provide Fortran and preliminary
Matlab
interfaces to these three new integrators. We also consider how sensitive such methods are to roundoff errors. Numerical results for four problems on a range of accuracy requests are presented.
Complex standard functions and their implementation in the CoStLy library
Authors: Neher Markus
Published: April 2007

The practical calculation of range bounds for some complex standard functions is addressed in this article. The functions under consideration are root and power functions, the exponential, trigonometric and hyperbolic functions, and their inverse functions. For such a function
f
and a given rectangular complex interval
z
, some interval
w
is computed that contains all function values of
f
in
z
. This is done by expressing the real and the imaginary part of
f
as compositions of real standard functions and then estimating the ranges of these compositions. In many cases, the inclusions are optimal, such that
w
is the smallest rectangular interval containing the range of
f
.

The algorithms presented in this article have been implemented in a C++ class library called CoStLy (
C
omplex
S
tandard Functions
L
icense), which is distributed under the conditions of the GNU General Public License.
Algorithm 864
Authors: Martello Silvano , Pisinger David , Vigo Daniele , Boef Edgar Den , Korst Jan
Published: April 2007

We consider the problem of orthogonally packing a given set of rectangular-shaped boxes into the minimum number of three-dimensional rectangular bins. The problem is NP-hard in the strong sense and extremely difficult to solve in practice. We characterize relevant subclasses of packing and present an algorithm which is able to solve moderately large instances to optimality. Extensive computational experiments compare the algorithm for the three-dimensional bin packing when solving general orthogonal packings and when restricted to robot packings.
Correspondence on Fortran standardization
Authors: Engle Frank
Published: April 2007

A letter by Howard Kaikow on Fortran standards for the order of evaluation of expressions appeared in the preceeding issue of this Newsletter. Mr. Kaikow had written a similar letter, in April, 1974, to Frank Engel, Jr. who is the chairman of the ANSI X3J3 Fortran Committee. Mr. Engel has kindly given permissio for the Newsleter to publish a copy of the response letter which he wrote to Mr. Kaikow in May, 1974.
A conjecture in numerical linear algebra
Authors: Farkas I.
Published: April 2007

In cca. Feb. 1971 when Wilkinson visited Toronto, I mentioned the following conjecture to him: Let us assume that we have a general complex matrix, then, the optimal way to determine its eigen system is Householder reduction followed by QR transformation in the sense of numerical analysis. Wilkinson remarked that the conjecture was too vague.
Power-efficient prefetching for embedded processors
Authors: Zhuang Xiaotong , Pande Santosh
Published: April 2007

Because of stringent power constraints, aggressive latency-hiding approaches, such as prefetching, are absent in the state-of-the-art embedded processors. There are two main reasons that make prefetching power inefficient. First, compiler-inserted prefetch instructions increase code size and, therefore, could increase I-cache power. Second, inaccurate prefetching (especially for hardware prefetching) leads to high D-cache power consumption because of useless accesses. In this work, we show that it is possible to support power-efficient prefetching through bit-differential offset assignment. We target the prefetching of relocatable stack variables with a high degree of precision. By assigning the offsets of stack variables in such a way that most consecutive addresses differ by 1 bit, we can prefetch them with compact prefetch instructions to save I-cache power. The compiler first generates an access graph of consecutive memory references and then attempts a layout of the memory locations in the smallest hypercube. Each dimension of the hypercube represents a 1-bit differential addressing. The embedding is carried out in as compact a hypercube as possible in order to save memory space. Each load/store instruction carries a hint regarding prefetching the next memory reference by encoding its differential address with respect to the current one. To reduce D-cache power cost, we further attempt to assign offsets so that most of the consecutive accesses map to the same cache line. Our prefetching is done using a one entry line buffer [Wilson et al. 1996]. Consequently, many look-ups in D-cache reduce to incremental ones. This results in D-cache activity reduction and power savings. Our prefetcher requires both compiler and hardware support. In this paper, we provide implementation on the processor model close to ARM with small modification to the ISA. We tackle issues such as out-of-order commit, predication, and speculation through simple modifications to the processor pipeline on noncritical paths. Our goal in this work is to boost performance while maintaining/lowering power consumption. Our results show 12% speedup and slight power reduction. The runtime virtual space loss for stack and static data is about 11.8%.
Link-time compaction and optimization of ARM executables
Authors: De Sutter Bjorn , Van Put Ludo , Chanet Dominique , De Bus Bruno , De Bosschere Koen
Published: April 2007

The overhead in terms of code size, power consumption, and execution time caused by the use of precompiled libraries and separate compilation is often unacceptable in the embedded world, where real-time constraints, battery life-time, and production costs are of critical importance. In this paper, we present our link-time optimizer for the ARM architecture. We discuss how we can deal with the peculiarities of the ARM architecture related to its visible program counter and how the introduced overhead can to a large extent be eliminated. Our link-time optimizer is evaluated with four tool chains, two proprietary ones from ARM and two open ones based on GNU GCC. When used with proprietary tool chains from ARM Ltd., our link-time optimizer achieved average code size reductions of 16.0 and 18.5%, while the programs have become 12.8 and 12.3% faster, and 10.7 to 10.1% more energy efficient. Finally, we show how the incorporation of link-time optimization in tool chains may influence library interface design.
Timing analysis for preemptive multitasking real-time systems with caches
Authors: Tan Yudong , Mooney Vincent
Published: April 2007

In this paper, we propose an approach to estimate the worst-case response time (WCRT) of each task in a preemptive multitasking single-processor real-time system utilizing an L1 cache. The approach combines intertask cache-eviction analysis and intratask cache-access analysis to estimate the number of cache lines that can possibly be evicted by the preempting task and also be accessed again by the preempted task after preemptions (thus requiring the preempted task to reload the cache line(s)). This cache-reload delay caused by preempting task(s) is then incorporated into WCRT analysis. Three sets of applications with up to six concurrent tasks running are used to test our approach. The experimental results show that our approach can tighten the WCRT estimate by up to 32% (1.4X) over prior state-of-the-art.
Safety verification of hybrid systems by constraint propagation-based abstraction refinement
Authors: Ratschan Stefan , She Zhikun
Published: April 2007

This paper deals with the problem of safety verification of nonlinear hybrid systems. We start from a classical method that uses interval arithmetic to check whether trajectories can move over the boundaries in a rectangular grid. We put this method into an abstraction refinement framework and improve it by developing an additional refinement step that employs interval-constraint propagation to add information to the abstraction without introducing new grid elements. Moreover, the resulting method allows switching conditions, initial states, and unsafe states to be described by complex constraints, instead of sets that correspond to grid elements. Nevertheless, the method can be easily implemented, since it is based on a well-defined set of constraints, on which one can run any constraint propagation-based solver. Tests of such an implementation are promising.
Wave scheduling and routing in sensor networks
Authors: Trigoni Niki , Yao Yong , Demers Alan , Gehrke Johannes , Rajaraman Rajmohan
Published: April 2007

Sensor networks are being increasingly deployed for diverse monitoring applications. Event data are collected at various sensors and sent to selected storage nodes for further in-network processing. Since sensor nodes have strong constraints on their energy usage, this data transfer needs to be energy-efficient to maximize network lifetime. In this article, we propose a novel methodology for trading energy versus latency in sensor database systems. We propose a new protocol that carefully schedules message transmissions so as to avoid collisions at the MAC layer. Since all nodes adhere to the schedule, their radios can be off most of the time and only wake up during well-defined time intervals. We show how routing protocols can be optimized to interact symbiotically with scheduling decisions, resulting in significant energy savings at the cost of higher latency. We demonstrate the effectiveness of our approach by means of a thorough simulation study, using synthetic data as well as real-world traffic workloads.
The Clustered AGgregation (CAG) technique leveraging spatial and temporal correlations in wireless sensor networks
Authors: Yoon Sunhee , Shahabi Cyrus
Published: April 2007

Sensed data in Wireless Sensor Networks (WSN) reflect the spatial and temporal correlations of physical attributes existing intrinsically in the environment. In this article, we present the Clustered AGgregation (CAG) algorithm that forms clusters of nodes sensing similar values within a given threshold (spatial correlation), and these clusters remain unchanged as long as the sensor values stay within a threshold over time (temporal correlation). With CAG, only one sensor reading per cluster is transmitted whereas with Tiny AGgregation (TAG) all the nodes in the network transmit the sensor readings. Thus, CAG provides energy efficient and approximate aggregation results with small and often negligible and bounded error.

In this article we extend our initial work in CAG in five directions: First, we investigate the effectiveness of CAG that exploits the temporal as well as spatial correlations using both the measured and modeled data. Second, we design CAG for two modes of operation (interactive and streaming) to enable CAG to be used in different environments and for different purposes. Interactive mode provides mechanisms for one-shot queries, whereas the streaming mode provides those for continuous queries. Third, we propose a fixed range clustering method, which makes the performance of our system independent of the magnitude of the sensor readings and the network topology. Fourth, using mica2 motes, we perform a large-scale measurement of real environmental data (temperature and light, both indoor and outdoor) and the wireless radio reliability, which were used for both analytical modeling and simulation experiments. Fifth, we model the spatially correlated data using the properties of our real world measurements.

Our experimental results show that when we compute the average of sensor readings in the network using the CAG interactive mode with the user-provided error threshold of, 20%, we can save 68.25% of transmissions over TAG with only 2.46% inaccuracy in the result. The streaming mode of CAG can save even more transmissions (up to 70.24% in our experiments) over TAG, when data shows high spatial and temporal correlations. We expect these results to hold in reality, because we used the mica2 radio profile and empirical datasets for our simulation study. CAG is the first system that leverages spatial and temporal correlations to improve energy efficiency of in-network aggregation. This study analytically and empirically validates CAG's effectiveness.
Analysis of the contention access period of IEEE 802.15.4 MAC
Authors: Ramachandran Iyappan , Das Arindam K. , Roy Sumit
Published: April 2007

The recent ratification of IEEE 802.15.4 PHY-MAC specifications for low-rate wireless personal area networks represents a significant milestone in promoting deployment of wireless sensor networks (WSNs) for a variety of commercial uses. The 15.4 specifications specifically target wireless networking among low-rate, low-power and low-cost devices that is expected to be a key market segment for a large number of WSN applications. In this article, we first analyze the performance of the contention access period specified in the IEEE 802.15.4 standard in terms of throughput and energy consumption. This analysis is facilitated by a modeling of the contention access period as nonpersistent CSMA with backoff. We show that, in certain applications in which having an inactive period in the superframe may not be desirable due to delay constraints, shutting down the radio between transmissions provides significant savings in power without significantly compromising the throughput. We also propose and analyze the performance of a modification to the specification which could be used for applications in which MAC-level acknowledgements are not used. Extensivens-2 simulations are used to verify the analysis.
A combinatorial algorithmic approach to energy efficient information collection in wireless sensor networks
Authors: Su Xun
Published: April 2007

In this article, we examine the energy consumption of a set of sensors that transmit correlated information to a base station either directly or in an ad-hoc multihop fashion. Building on a single-hop distributed data rate allocation scheme, we present an efficient approximation algorithm for the NP-hard joint routing and data compression problem whose objective is to maximize the operation lifetime of the sensor networks. We prove that the performance of our algorithm lies within 1/
O
(log
n
) of the optimum value where
n
is the number of sensors. We use simulations to validate our intuitions and provide additional insights on the factors that impact the performance of the approximation scheme. The numerical results show that the proposed scheme performs close to the optimum.
Cyberethics bibliography 2005
Authors: Tavani Herman T.
Published: April 2007

Included in the 2005 cyberethics bibliography update is an annotated list of more than fifty recent books; each has a publisher's date of 2002 or later. This list expands upon the books identified and annotated in cyberethics bibliography included in the June 2003 issue of
ACM Computers and Society Magazine
. For information about selected books published between 1998 and 2002, see the June 1999, June 2000, June 2001, and June 2002 issues of
Computers and Society;
and for a comprehensive list of books and articles published before 1997, see my
Computing, Ethics, and Social Responsibility: A Bibliography
(available at http://cyberethics.cbi.msstate.edu/biblio).
Some information is too dangerous to be on the internet
Authors: Müller Vincent C.
Published: April 2007

This paper investigates a problem about freedom of information. Although freedom of information is generally considered desirable, there are a number of areas where there is substantial agreement that freedom of information should be limited. After a certain ordering of the landscape, I argue that we need to add the category of 'dangerous' information and that this category has gained a new quality in the context of current information technology, specifically the Internet. This category includes information the use of which would be morally wrong as well as some of what may be called 'corrupting' information. Some such information should not be spread at all and some should be very limited in its spread.
Public involvement in technology policy
Authors: Winter Jenifer S.
Published: April 2007

This paper examines the role of the general public in informing technology policy, observing that public involvement often occurs only through the electoral process or via feedback after plans have been implemented. Planners and policymakers are not necessarily in touch with the feelings and desires of the public who will be affected by their decisions. For this reason it is important to seek a clearer understanding of the views of citizens who are not typically involved in the planning or design process in order to guide the evolution of technology, as well as to highlight areas where there may be some discrepancy between planners and the needs of everyday users. To broaden the inputs into discussion of emerging problems related to pervasive computing in the State of Hawaii, both information and communication technology specialists (including government policy makers) and members of the general population were invited to participate in a multi-phase study. Differences in perception between specialists and the general public were identified in all phases of research. Specialists were identified as being more focused on near-term issues related to barriers affecting the growth of high-technology industries within the State. Non-specialists showed greater concern for "human" issues, including issues related to the control of technology. Importantly, both groups independently described a need for increased public participation in the process of technological development. Analysis also revealed that both groups found the problem statements generated by non-specialists to be valuable contributions, arguing for their inclusion in the process of problem identification and further supporting the use of participatory planning methods.
Computer sciences and commercial forces
Authors: Ophir Shai
Published: April 2007

Computer Sciences (CS) are having a major impact on recent scientific developments. As any other basic science, the CS is publicly perceived as an open and free science that is trying to make progress in any possible direction, resolving scientific problems in its arena and dealing with pure scientific and issues and theoretical questions per se. In this paper I claim that this is not the case. CS is heavily controlled by commercial forces, which dictate its progress, goals and future directions. The new developments in the CS arena are in most cases the result of the market needs. Several research projects at the universities are funded by the industry, dealing with issues with a clear industrial aspect. Public funds, such as the 6
th
European Framework project allocates a major portion of their funds for industrial research. The IEEE and ACM, the most respectful technology organizations of the CS, are governed by the industry and the universities at about equal share. The industry is holding patent rights for several CS research results, and CS scientists are issuing patents for their research because it may have a significant economic value. The CS is not an open science, in terms of Popper definition.
Analysis of a transmission scheduling algorithm for supporting bandwidth guarantees in bufferless networks
Authors: Elhaddad Mahmoud , Melhem Rami , Znati Taieb
Published: April 2007

In a network of bufferless packet multiplexers, the user-perceived capacity of an ingress-egress tunnel (connection) may degrade quickly with increasing path length. This is due to the compounding of transmission blocking probabilities along the path of the connection, even when the links are not overloaded. In such an environment, providing users (e.g., client ISPs) with tunnels of statistically guaranteed bandwidth may limit the network's connection-carrying capacity.In this paper, we introduce and analyze a transmission-scheduling algorithm that employs randomization and traffic regulation at the ingress, and batch scheduling at the links. The algorithm ensures that a fraction of transmissions from each connection is consistently subject to small blocking probability at every link, so that these transmissions are likely to survive long paths. For this algorithm, we obtain tight bounds on the expectation and tail probability of the blocking rate of any ingress-egress connection. We compare the bounds to those obtained using the FCFS link-scheduling rule. We find that the proposed scheduling algorithm significantly improves the network's connection-carrying capacity.In deriving the desired bounds, we develop an analytic framework for stochastically comparing network-wide routing and bandwidth allocation scenarios with respect to blocking in a packet multiplexer. The framework enables us to formally characterize the routing and bandwidth allocation scenarios that maximize the expected blocking rate along the path of a tagged connection.
Foreword
Authors: Squillante Mark S.
Published: April 2007

The complexity of computer systems, networks and applications, as well as the advancements in computer technology, continue to grow at a rapid pace. Mathematical analysis, modeling and optimization have been playing, and continue to play, an important role in research studies to investigate fundamental issues and tradeoffs at the core of performance problems in the design and implementation of complex computer systems, networks and applications.
Towards power and QoS aware wireless networks
Authors: Nakassis Anastase , Marbukh Vladimir
Published: April 2007

The paper studies the optimal use of energy in wireless networking, the feasibility region of tasks that share a multi-access channel, and efficient algorithms for determining if a given set of tasks and resources falls within the feasibility region.
Exact probability distributions for peer-to-peer epidemic information diffusion
Authors: Yazici Emine Şule , Küçükçifçi Selda , Özkasap Öznur , Çaǧlar Mine
Published: April 2007

An efficient approach for information diffusion in distributed systems is to utilize epidemic algorithms that involve pair-wise propagation of updates. Epidemic algorithms are fully distributed and randomized approaches such that every peer in an information diffusion session picks a (subset of the other) peer(s) randomly for efficient propagation of updates, through periodic rounds. The underlying epidemics theory for the biological systems studies the spreading of infectious diseases through a population [1,2]. When applied to an information diffusion application, such protocols have beneficial features such as scalability, robustness against failures and provision of eventual consistency. Exact as well as asymptotical distributions have been studied for different epidemic models in [3,4]. In contrast to such previous studies, we investigate variations of the epidemic algorithms used in the context of distributed information diffusion and derive exact diffusion probabilities for them.
Media overlay construction via a Markov chain Monte Carlo method
Authors: Luan Hao , Tsang Danny H. K. , Kwong Kin Wah
Published: April 2007

In this paper, we consider the fairness issue of BT and tackle the problem with a general framework using proactive topology adaptations. The topology formed possesses a special link-level homogeneity property with each peer having the same capacity per out-degree value. Such property guarantees that each directional link has the same uploading bandwidth. Together with the Tit-for-Tat policy, peers upload and download at the same rate over each connection and therefore achieve fairness.
On the effect of inexact size information in size based policies
Authors: Wierman Adam
Published: April 2007

Recently, there have been a number of scheduling success stories in computer applications. Across a wide array of applications, the simple heuristic of "prioritizing small jobs" has been used to reduce user response times with enormous success. For instance, variants of Shortest-Remaining-Processing-Time (SRPT) and Preemptive-Shortest-Job-First (PSJF) have been suggested for use in web servers [5, 12], wireless applications [6], and databases [8]. As a result of the attention given to size based policies by computer systems researchers, there has been a resurgence in analytical work studying these policies. However, the policies studied in theory, e.g. SRPT and PSJF, are idealized versions of the policies implemented by practitioners. In particular, the intricacies of computer systems force the use of complex hybrid policies in practice, though these more complex policies are still built around the heuristic of "prioritizing small jobs." Thus, there exists a gap between the results provided by theoretical research and the needs of practitioners. This gap results from three primary disconnects between the model studied in theory and the needs of system designers. First, in designing systems, the goal is not simply to provide small response times; other performance measures are also important. Thus, idealized policies such as SRPT and PSJF are often tweaked by practitioners to perform well on secondary performance measures (e.g. fairness and slowdown) [3, 11, 12]. Second, the overhead involved in distinguishing between an infinite number of different priority classes typically causes system designers to discretize policies such as SRPT and PSJF so that they use only a small number of priority classes (5-10) [5, 11]. Third, in many cases information about the service demands (sizes) of jobs is inexact. For instance, when serving static content, web servers have exact knowledge of the sizes of the files being served, but have inexact knowledge of network conditions. Thus, the web server only has an estimate of the true service demand [7, 12].
Stationarity of some processes in transport protocols
Authors: Ott Teunis J. , Swanson Jason
Published: April 2007

This note establishes stationarity of a number of stochastic processes of interest in the study of Transport Protocols. For many of the processes studied in this note stationarity had been established before, but for one class the result is new. For that class, it was counterintuitive that stationarity was hard to prove. This note also explains why that class offered such stiff resistance.The stationarity is proven using Liapunov functions, without first proving tightness by proving boundedness of moments. After the 2006 MAMA workshop simple conditions for existence of such moments were obtained and were added to this note.
Finding probably best system configurations quickly
Authors: Osogami Takayuki
Published: April 2007

Computer systems often have many possible configurations, and designing a high performance system often requires selecting the best configuration. Unfortunately, the performance of complex systems can often be estimated only via simulations, or with measurements of real systems. Since longer simulation times are required to estimate the performance more accurately, it is often computationally intractable to estimate the performance of all configurations accurately via simulations. (Measurements of real systems can take even longer.)
Asymptotic optimality of threshold control in a stochastic network based on a fixed-point approximation
Authors: Yao David D. , Ye Heng-Qing
Published: April 2007

In Li and Yao [5], a stochastic network with simultaneous resource occupancy is studied, and a threshold control policy is proposed based on a fixed-point approximation. Here, we establish the asymptotic optimality of this control policy under fluid and diffusion scaling.
Load-balanced routing for mesh networks
Authors: Yang Yaling , Wang Jun , Kravets Robin
Published: April 2007

Due to the static nature of nodes, in mesh networks, a poor choice of paths may remain unchanged for a long time and create hot spots. Hence, it is very important to design path weight functions (also called routing metrics) to facilitate load-balanced routing in mesh networks. Such path weight functions (PWFs) must reflect the shared nature of wireless channels and support easy calculation of loop-free paths. In this abstract, we present our theoretical studies of the requirements on PWFs and design the first PWF, called
Metric of Interference and Channel-switching (MIC)
, that satisfies these requirements. Our simulation results show that MIC's performance is substantially better than existing PWFs. (See our technical report [5] for more details.)
Wireless operators in a shared spectrum
Authors: Felegyhazi Mark , Hubaux Jean-Pierre
Published: April 2007

Cellular networks are notoriously difficult to design and operate; in particular, defining the optimal location of the base stations and fine tuning their configuration parameters is very challenging. For this reason, government agencies (such as the FCC for the US) usually sell or rent, for example by auction, each operator a frequency band for its exclusive usage in a given country or region. Only a small part of the whole spectrum is allocated as a
shared spectrum
, in which networks function in the same (unlicensed) frequency band.
S-EDCA: EDCA based on SuperSlot and Pseudo Collision
Authors: Ryu Jiho , Seok Yongho , Choi Nakjung , Kwon Taekyoung , Choi Yanghee
Published: April 2007

The IEEE 802.11e EDCA mechanism cannot guarantee the QoS of high-priority traffic as the bandwidth consumption of low-priority traffic increases. Also, the existence of high priority traffic undermines link utilization of low priority traffic. To solve these problems, we propose the S-EDCA
scheme that extends IEEE 802.11e EDCA by introducing a
SuperSlot
and
Pseudo Collision.
Compared to IEEE 802.11e EDCA
, S-EDCA has two advantages: (a) Higher priority traffic achieves QoS regardless of the amount of low priority traffic, and (b) Low priority traffic experiences a higher throughput with the same amount of high priority traffic.
Studying vehicle movements on highways and their impact on ad-hoc connectivity
Authors: Füßler Holger , Torrent-Moreno Marc , Transier Matthias , Krüger Roland , Hartenstein Hannes , Effelsberg Wolfgang
Published: April 2007

The mobility of the nodes in a Mobile Ad-Hoc Network (MANET) is a crucial factor in the performance studies of communication protocols for these kind of networks. For this reason, researchers usually use a randomized node movement model, such as the Random Way-Point Model [6], in the process of designing or analyzing the behavior of their protocols. Since movement is not very predictable in these scenarios, they generally serve as a "worst case assumption" of node mobility concerning communication protocol performance in the sense that a positive correlation between performance in an RWP scenario and an arbitrary scenario exists. Additionally, RWP is an analytically well-understood mobility scheme and the movements can be generated very easily with tools complementary to most of the common network simulators.
Mobile ad hoc networking and the IETF
Authors: Chakeres Ian D. , Macker Joseph P.
Published: April 2007

This article is part of a continuing series to discuss ongoing activities within the mobile ad hoc networking (MANET) working group (WG) of the IETF. This article provides a brief overview of recent events.
Spam and the ongoing battle for the inbox
Authors: Goodman Joshua , Cormack Gordon V. , Heckerman David
Published: April 2007

Even as spammers and phishers try evermore sophisticated techniques to get past filters and into users' mailboxes, anti-spam researchers have managed to stay several steps ahead, so far.
Compliance with the CAN-SPAM Act of 2003
Authors: Grimes Galen A.
Published: April 2007

Studying the application of the CAN-SPAM Act and its effect on controlling unsolicited email messages.
Encouraging participation in virtual communities
Authors: Koh Joon , Kim Young-Gul , Butler Brian , Bock Gee-Woo
Published: April 2007

Leaders of robust, sustainable virtual communities find ways tostrengthen their members' sense of social identity and motivate their participation in the community's activities.