Despite the importance of elections in India, the world's largest democracy, data on Indian electoral outcomes has not been easily available for political analysis in the past. This has been due to the problems inherent in assembling any data archive of social and political data spanning many decades. In this paper, we shed some light on these problems and present some solutions in the context of a system we built called LokDhaba. LokDhaba includes the first freely-available, structured and cleaned data archive on Indian electoral outcomes at the national or state level from 1962 onwards. To build this archive, we overcame the challenges of data scraping, parsing, cleaning, consistency checking and integration between multiple sources, with the help of some novel tools. LokDhaba is being used extensively by political scientists, researchers, journalists and others to better understand long-term electoral trends in India.

People often find useful content on the web via social media. However, it is difficult for users to aggregate the information and recommendations embedded in a torrent of social feeds like email and Twitter. At the same time, the ever-growing size of the web and attempts to spam commercial search engines make it a challenge for users to get search results relevant to their unique background and interests. To address this problem, we propose ways to let users mine their own social chatter and extract people, pages and sites of potential interest. This information can be used to effectively personalize their web search results. Our approach has the benefits of generating personalized and socially curated results, removing web spam and preserving user privacy.

In the digital age, users can have perfect recall of their online experiences. In this paper, we explore how this recall can be leveraged during web browsing.

As people accumulate hundreds of "friends" in social media, a flat list of connections becomes unmanageable. Interfaces agnostic to social structure hinder the nuanced sharing of personal data such as photos, status updates, news feeds, and comments. To address this problem, we propose social topologies, a set of potentially overlapping and nested social groups, that represent the structure and content of a person's social network as a first-class object. We contribute an algorithm for creating social topologies by mining communication history and identifying likely groups based on co-occurrence patterns. We use our algorithm to populate a browser interface that supports creation and editing of social groups via direct manipulation. A user study confirms that our approach models subjects' social topologies well, and that our interface enables intuitive browsing and management of a personal social landscape.

Email archives silently record our actions and thoughts over the years, forming a passively acquired and detailed life-log that contains rich material for reminiscing on our lives. However, exploratory browsing of archives containing thousands of messages is tedious without effective ways to guide the user towards interesting events and messages. We present Muse (Memories USing Email), a system that combines data mining techniques and an interactive interface to help users browse a long-term email archive. Muse analyzes the contents of the archive and generates a set of cues that help to spark users' memories: communication activity with inferred social groups, a summary of recurring named entities, occurrence of sentimental words, and image attachments. These cues serve as salient entry points into a browsing interface that enables faceted navigation and rapid skimming of email messages. In our user studies, we found that users generally enjoyed browsing their archives with Muse, and extracted a range of benefits, from summarizing work progress to renewing friendships and making serendipitous discoveries.

This paper introduces UniFi, a tool that attempts to automatically detect dimension errors in Java programs. UniFi infers dimensional relationships across primitive type and string variables in a program, using an inter-procedural, context-sensitive analysis. It then monitors these dimensional relationships as the program evolves, flagging inconsistencies that may be errors. UniFi requires no programmer annotations, and supports arbitrary program-specific dimensions, thus providing fine-grained dimensional consistency checking. UniFi exploits features of object-oriented languages, but can be used for other languages as well. We have run UniFi on real-life Java code and found that it is useful in exposing dimension errors. We present a case study of using UniFi on nightly builds of a 19,000 line code base as it evolved over 10 months.

Transactional memory is an attractive design concept for scalable multiprocessors because it offers efficient lock-free synchronization and greatly simplifies parallel software. Given the subtle issues involved with concurrency and atomicity, however, it is important that transactional memory systems be carefully designed and aggressively tested to ensure their correctness. In this paper, we propose an axiomatic framework to model the formal specification of a realistic transactional memory system which may contain a mix of transactional and non-transactional operations. Using this framework and extensions to analysis algorithms originally developed for checking traditional memory consistency, we show that the widely practiced pseudo-random testing methodology can be effectively applied to transactional memory systems. Our testing methodology was successful in finding previously unknown bugs in the implementation of TCC, a transactional memory system. We study two flavors of the underlying analysis algorithm, one incomplete and the other complete, and show that the complete algorithm while being theoretically intractable is very efficient in practice.

An important means of validating the design of commercial-grade shared memory multiprocessors is to run a large number of pseudo-random test programs on them. However, when intentional data races are placed in a test program, there may be many correct results according to the memory consistency model supported by the system. For popular memory models like SC and TSO, the problem of verifying correctness of an execution is known to be NP-complete. As a result, analysis techniques implemented in the past have been incomplete: violations of the memory model are flagged if provable, otherwise the result is inconclusive and it is assumed optimistically that the machine's results are correct. In this paper, we describe for the first time a practical, new algorithm which can solve this problem with certainty, thus ensuring that incorrect behavior of a large, complex multiprocessor cannot escape. We present results of our analysis algorithm on test programs run on a newly designed multiprocessor system built by Sun Microsystems. We show that our algorithm performs very well, typically analyzing a program with 512 K memory operations distributed across 60 processors within a few minutes. Our algorithm runs in less than 2.6 times the time taken by an incomplete baseline algorithm which may miss errors. Our approach greatly increases the confidence in the correctness of the results generated by the multiprocessor, and allows us to potentially uncover more bugs in the design than was previously possible.

We describe IODINE, a tool to automatically extract likely design properties using dynamic analysis. A practical bottleneck in the formal verication of hardware designs is the need to manually specify design-specic properties. IODINE presents a way to automatically extract properties such as state machine protocols, request-acknowledge pairs, and mutual exclusion between signals from design simulations. We show that dynamic invariant detection for hardware designs can infer relevant and accurate properties.

One approach in verifying the correctness of a multiprocessor system is to show that its execution results comply with the memory consistency model it is meant to implement. It has been shown in prior work, however, that accurately verifying such compliance even of a single execution result is an NP-complete problem, for an unlimited number of processors. In this paper, we present a suite of post-mortem algorithms that perform the compliance check in an efficient, although not exhaustive, manner. Our algorithms employ the concept of vector clocks together with a heuristic made from a variation of the problem in P class. An implementation of these algorithms has been successful in efficiently detecting several bugs during the course of validating the design of commercial microprocessors and systems.Although our algorithms are presented with the Total Store Order (TSO) memory model, the ideas can also be applied to other models ranging from Sequential Consistency (SC) to a more relaxed one such as Relaxed Memory Order (RMO).

In this paper, we describe TSOtool, a program to check the behavior of the memory subsystem in a shared memory multiprocessor. TSOtool runs pseudo-randomly generated programs with data races on a system compliant with the total store order (TSO) memory consistency model; it then checks the results of the program against the formal TSO specification. Such analysis can expose subtle memory errors like data corruption, atomicity violation and illegal instruction ordering. While verifying TSO compliance completely is an NP-complete problem, we describe a new polynomial time algorithm which is incorporated in TSOtool. In spite of being incomplete, it has been successful in detecting several bugs in the design of commercial microprocessors and systems, during both pre-silicon and post-silicon phases of validation.

This paper introduces DIDUCE, a practical and effective tool that aids programmers in detecting complex program errors and identifying their root causes. By instrumenting a program and observing its behavior as it runs, DIDUCE dynamically formulates hypotheses of invariants obeyed by the program. DIDUCE hypothesizes the strictest invariants at the beginning, and gradually relaxes the hypothesis as violations are detected to allow for new behavior. The violations reported help users to catch software bugs as soon as they occur. They also give programmers new visibility into the behavior of the programs such as identifying rare corner cases in the program logic or even locating hidden errors that corrupt the program's results.We implemented the DIDUCE system for Java programs and applied it to four programs of significant size and complexity. DIDUCE succeeded in identifying the root causes of programming errors in each of the programs quickly and automatically. In particular, DIDUCE is effective in isolating a timing-dependent bug in a released JSSE (Java Secure Socket Extension) library, which would have taken an experienced programmer days to find. Our experience suggests that detecting and checking program invariants dynamically is a simple and effective methodology for debugging many different kinds of program errors across a wide variety of application domains.