No Arabic abstract
A consistent theme in software experimentation at Microsoft has been solving problems of experimentation at scale for a diverse set of products. Running experiments at scale (i.e., many experiments on many users) has become state of the art across the industry. However, providing a single platform that allows software experimentation in a highly heterogenous and constantly evolving ecosystem remains a challenge. In our case, heterogeneity spans multiple dimensions. First, we need to support experimentation for many types of products: websites, search engines, mobile apps, operating systems, cloud services and others. Second, due to the diversity of the products and teams using our platform, it needs to be flexible enough to analyze data in multiple compute fabrics (e.g. Spark, Azure Data Explorer), with a way to easily add support for new fabrics if needed. Third, one of the main factors in facilitating growth of experimentation culture in an organization is to democratize metric definition and analysis processes. To achieve that, our system needs to be simple enough to be used not only by data scientists, but also engineers, product managers and sales teams. Finally, different personas might need to use the platform for different types of analyses, e.g. dashboards or experiment analysis, and the platform should be flexible enough to accommodate that. This paper presents our solution to the problems of heterogeneity listed above.
The concurrency features of the Go language have proven versatile in the development of a number of concurrency systems. However, correctness methods to address challenges in Go concurrency debugging have not received much attention. In this work, we present an automatic dynamic tracing mechanism that efficiently captures and helps analyze the whole-program concurrency model. Using an enhancement to the built-in tracer package of Go and a framework that collects dynamic traces from application execution, we enable thorough post-mortem analysis for concurrency debugging. Preliminary results about the effectiveness and scalability (up to more than 2K goroutines) of our proposed dynamic tracing for concurrent debugging are presented. We discuss the future direction for exploiting dynamic tracing towards accelerating concurrent bug exposure.
A new approach called RESID is proposed in this paper for estimating reliability of a software allowing for imperfect debugging. Unlike earlier approaches based on counting number of bugs or modelling inter-failure time gaps, RESID focuses on the probability of bugginess of different parts of a program buggy. This perspective allows an easy way to incorporate the structure of the software under test, as well as imperfect debugging. One main design objective behind RESID is ease of implementation in practical scenarios.
We present an approach to estimate distance-dependent heterogeneous associations between point-referenced exposures to built environment characteristics and health outcomes. By estimating associations that depend non-linearly on distance between subjects and point-referenced exposures, this method addresses the modifiable area-unit problem that is pervasive in the built environment literature. Additionally, by estimating heterogeneous effects, the method also addresses the uncertain geographic context problem. The key innovation of our method is to combine ideas from the non-parametric function estimation literature and the Bayesian Dirichlet process literature. The former is used to estimate nonlinear associations between subjects outcomes and proximate built environment features, and the latter identifies clusters within the population that have different effects. We study this method in simulations and apply our model to study heterogeneity in the association between fast food restaurant availability and weight status of children attending schools in Los Angeles, California.
Recently, we developed an automated theorem prover for projective incidence geometry. This prover, based on a combinatorial approach using matroids, proceeds by saturation using the matroid rules. It is designed as an independent tool, implemented in C, which takes a geometric configuration as input and produces as output some Coq proof scripts: the statement of the expected theorem, a proof script proving the theorem and possibly some auxiliary lemmas. In this document, we show how to embed such an external tool as a plugin in Coq so that it can be used as a simple tactic.
With the popularity of Android apps, different techniques have been proposed to enhance app protection. As an effective approach to prevent reverse engineering, obfuscation can be used to serve both benign and malicious purposes. In recent years, more and more sensitive logic or data have been implemented as obfuscated native code because of the limitations of Java bytecode. As a result, native code obfuscation becomes a great obstacle for security analysis to understand the complicated logic. In this paper, we propose DiANa, an automated system to facilitate the deobfuscation of native binary code in Android apps. Specifically, given a binary obfuscated by Obfuscator-LLVM (the most popular native code obfuscator), DiANa is capable of recovering the original Control Flow Graph. To the best of our knowledge, DiANa is the first system that aims to tackle the problem of Android native binary deobfuscation. We have applied DiANa in different scenarios, and the experimental results demonstrate the effectiveness of DiANa based on generic similarity comparison metrics.