Microsoft Research Love: More Goodness

MSR-TR-2008-153

Path Feasibility Analysis for String-Manipulating Programs
Nikolaj Bjorner; Nikolai Tillmann; Andrei Voronkov
October 2008
16 p.
https://research.microsoft.com/research/pubs/view.aspx?tr_id=1570
We discuss the problem of path feasibility for programs manipulating strings using a collection of standard string library functions. We prove results on the complexity of this problem, including its undecidability in the general case and decidability of some special cases. In the context of test-case generation, we are interested in an efficient finite model finding method for string constraints. To this end we develop a two-tier finite model finding procedure. First, an integer abstraction of string constraints are passed to an SMT (Satisfiability Modulo Theories) solver. The abstraction is either unsatisfiable, or the solver produces a model that fixes lengths of enough strings to reduce the entire problem to be finite domain. The resulting fixed-length string constraints are then solved in a second phase. We implemented the procedure in a symbolic execution framework, report on the encouraging results and discuss directions for improving the method further.

MSR-TR-2008-152

Lightweight Software Transactions for Games
Sebastian Burckhardt; Alexandro Baldassin
October 2008
5 p.
https://research.microsoft.com/research/pubs/view.aspx?tr_id=1569
To realize the performance potential of multiple cores, software developers must architect their programs for concurrency. Unfortunately, for many applications, threads and locks are difficult to use efficiently and correctly. Thus, researchers have proposed transactional memory as a simpler alternative. To investigate if and how software transactional memory (STM) can help a programmer to parallelize applications, we perform a case study on a game application called SpaceWars3D. After experiencing suboptimal performance, we depart from classic STM designs and propose a programming model that uses long-running, abort-free transactions that rely on user specifications to avoid or resolve conflicts. With this model we achieve the combined goal of competitive performance and improved programmability.

MSR-TR-2008-150

Persistent Queries
Andreas Blass; Yuri Gurevich
October 2008
41 p.
https://research.microsoft.com/research/pubs/view.aspx?tr_id=1567
We propose a syntax and semantics for interactive abstract state machines to deal with the following situation. A query is issued during a certain step, but the step ends before any reply is received. Later, a reply arrives, and later yet the algorithm makes use of this reply. By a persistent query, we mean a query for which a late reply might be used. Syntactically, our proposal involves issuing, along with a persistent query, a location where a late reply is to be stored. Semantically, it involves only a minor modification of the existing theory of interactive small-step abstract state machines.

MSR-TR-2008-149

Opportunistic Use of Client Repeaters to Improve Performance of WLANs
Victor Bahl; Ranveer Chandra; Patrick Lee; Vishal Misra; Jitendra Padhye; Dan Rubenstein; Yan Yu
October 2008
14 p.
https://research.microsoft.com/research/pubs/view.aspx?tr_id=1566
Currently deployed IEEE 802.11WLANs (Wi-Fi networks) share access point (AP) bandwidth on a per-packet basis. However, the various stations communicating with the AP often have different signal qualities, resulting in different transmission rates. This induces a phenomenon known as the rate anomaly problem, in which stations with lower signal quality transmit at lower rates and consume a significant majority of airtime, thereby dramatically reducing the throughput of stations transmitting at high rates. We propose a practical, deployable system, called Soft- Repeater, in which stations cooperatively address the rate anomaly problem. Specifically, higher-rate Wi-Fi stations opportunistically transformthemselves into repeaters for stations with low data-rates when transmitting to/from the AP. The key challenge is to determine when it is beneficial to enable the repeater functionality. In this paper, we propose an initiation protocol that ensures that repeater functionality is enabled only when appropriate. Also, our system can run directly on top of today’s 802.11 infrastructure networks. We evaluate our system using simulation and testbed implementation, and find that SoftRepeater can improve cumulative throughput by up to 200%.

MSR-TR-2008-148

Towards Unified Management of Networked Services in Wired and Wireless Networks
Victor Bahl; Ranveer Chandra; Dave Maltz; Parveen Patel; Jitendra Padhye
October 2008
14 p.
https://research.microsoft.com/research/pubs/view.aspx?tr_id=1565
Organizations world-wide are adopting wireless networks at an impressive rate, and a new industry has sprung up to provide tools to manage these networks. Unfortunately, these tools do not integrate cleanly with traditional wired network management tools, leading to unsolved problems and frustration among the IT staff. We explore the problem of unifying wireless and wired network management and show that simple merging of tools and strategies, and/or their trivial extension from one domain to another does not work. Building on previous research on network service dependency extraction, fault diagnosis, and wireless network management, we introduce MnM, an endto- end network management system that unifies wired and wireless network management. MnM treats physical location of end devices as a core component of its management strategy. It also dynamically adapts to the frequent topology changes brought about by end-node mobility.We have a prototype deployment in a large organization that shows that MnM’s root-cause analysis engine easily out-performs systems that do not take user mobility into account in terms of correctly localizing faults and blame attribution.