bluuebunny/crossref_metadata_2025 huggingface dataset:
The Representation of East Asia in Latin American Legislatures
Authors: KIKUCHI HIROKAZU
Published: October 2017

What is the representation of East Asia in Latin American legislatures? Existing studies have focused on individual politicians of East Asian descent such as Alberto Fujimori, former president of Peru, but no systematic research has been done on the political representation of East Asia in Latin America. In order to fill this gap, this study analyzes the descriptive and substantive aspects of East Asian representation in Latin America. For the descriptive dimension, this article reviews the composition of legislators of East Asian descent in each Latin American country and finds that people of Japanese descent are “overrepresented” in the Peruvian and Argentine lower houses, while people of Korean and Chinese descent are underrepresented. Using the Brazilian Chamber of Deputies as an example, this study also reveals that deputies of East Asian descent differ from other deputies in terms of their political careers. As for the substantive dimension, this study focuses on Brazilian deputies’ responses to the Twin Ocean Railroad project, one of the largest Chinese infrastructure projects in Latin America. The statistical test performed in this study shows that the deputies tend to be members of the Brazil–Peru–China Pro-Twin Ocean Railroad Caucus if they are affiliated with the Brazil–Japan Caucus, if they are from a wealthier state, or if their performance in the last election was good. In addition, they are not likely to be members of the caucus if they are affiliated with the Partido da Social Democracia Brasileira (PSDB), an important opposition party.
A simple soundness proof for dependent object types
Authors: Rapoport Marianna , Kabir Ifaz , He Paul , Lhoták Ondřej
Published: October 2017

Dependent Object Types (DOT) is intended to be a core calculus for modelling Scala. Its distinguishing feature is abstract type members, fields in objects that hold types rather than values. Proving soundness of DOT has been surprisingly challenging, and existing proofs are complicated, and reason about multiple concepts at the same time (e.g. types, values, evaluation). To serve as a core calculus for Scala, DOT should be easy to experiment with and extend, and therefore its soundness proof needs to be easy to modify.

This paper presents a simple and modular proof strategy for reasoning in DOT. The strategy separates reasoning about types from other concerns. It is centred around a theorem that connects the full DOT type system to a restricted variant in which the challenges and paradoxes caused by abstract type members are eliminated. Almost all reasoning in the proof is done in the intuitive world of this restricted type system. Once we have the necessary results about types, we observe that the other aspects of DOT are mostly standard and can be incorporated into a soundness proof using familiar techniques known from other calculi.
A volatile-by-default JVM for server applications
Authors: Liu Lun , Millstein Todd , Musuvathi Madanlal
Published: October 2017

A *memory consistency model* (or simply *memory model*) defines the possible values that a shared-memory read may return in a multithreaded programming language. Choosing a memory model involves an inherent performance-programmability tradeoff. The Java language has adopted a *relaxed* (or *weak*) memory model that is designed to admit most traditional compiler optimizations and obviate the need for hardware fences on most shared-memory accesses. The downside, however, is that programmers are exposed to a complex and unintuitive semantics and must carefully declare certain variables as `volatile` in order to enforce program orderings that are necessary for proper behavior.

This paper proposes a simpler and stronger memory model for Java through a conceptually small change: *every* variable has `volatile` semantics by default, but the language allows a programmer to tag certain variables, methods, or classes as `relaxed` and provides the current Java semantics for these portions of code. This *volatile-by-default* semantics provides *sequential consistency* (SC) for all programs by default. At the same time, expert programmers retain the freedom to build performance-critical libraries that violate the SC semantics.

At the outset, it is unclear if the `volatile`-by-default semantics is practical for Java, given the cost of memory fences on today's hardware platforms. The core contribution of this paper is to demonstrate, through comprehensive empirical evaluation, that the `volatile`-by-default semantics is arguably acceptable for a predominant use case for Java today -- server-side applications running on Intel x86 architectures. We present VBD-HotSpot, a modification to Oracle's widely used HotSpot JVM that implements the `volatile`-by-default semantics for x86. To our knowledge VBD-HotSpot is the first implementation of SC for Java in the context of a modern JVM. VBD-HotSpot incurs an average overhead versus the baseline HotSpot JVM of 28% for the Da Capo benchmarks, which is significant though perhaps less than commonly assumed. Further, VBD-HotSpot incurs average overheads of 12% and 19% respectively on standard benchmark suites for big-data analytics and machine learning in the widely used Spark framework.
Static placement of computation on heterogeneous devices
Authors: Poesia Gabriel , Guimarães Breno , Ferracioli Fabrício , Pereira Fernando Magno Quintão
Published: October 2017

Heterogeneous architectures characterize today hardware ranging from super-computers to smartphones. However, in spite of this importance, programming such systems is still challenging. In particular, it is challenging to map computations to the different processors of a heterogeneous device. In this paper, we provide a static analysis that mitigates this problem. Our contributions are two-fold: first, we provide a semi-context-sensitive algorithm, which analyzes the program's call graph to determine the best processor for each calling context. This algorithm is parameterized by a cost model, which takes into consideration processor's characteristics and data transfer time. Second, we show how to use simulated annealing to calibrate this cost model for a given heterogeneous architecture. We have used our ideas to build Etino, a tool that annotates C programs with OpenACC or OpenMP 4.0 directives. Etino generates code for a CPU-GPU architecture without user intervention. Experiments on classic benchmarks reveal speedups of up to 75x. Moreover, our calibration process lets avoid slowdowns of up to 720x which trivial parallelization approaches would yield.
Model checking copy phases of concurrent copying garbage collection with various memory models
Authors: Ugawa Tomoharu , Abe Tatsuya , Maeda Toshiyuki
Published: October 2017

Modern concurrent copying garbage collection (GC), in particular, real-time GC, uses fine-grained synchronizations with a mutator, which is the application program that mutates memory, when it moves objects in its copy phase. It resolves a data race using a concurrent copying protocol, which is implemented as interactions between the collector threads and the read and write barriers that the mutator threads execute. The behavioral effects of the concurrent copying protocol rely on the memory model of the CPUs and the programming languages in which the GC is implemented. It is difficult, however, to formally investigate the behavioral properties of concurrent copying protocols against various memory models.

To address this problem, we studied the feasibility of the bounded model checking of concurrent copying protocols with memory models. We investigated a correctness-related behavioral property of copying protocols of various concurrent copying GC algorithms, including real-time GC Stopless, Clover, Chicken, Staccato, and Schism against six memory models, total store ordering (TSO), partial store ordering (PSO), relaxed memory ordering (RMO), and their variants, in addition to sequential consistency (SC) using bounded model checking. For each combination of a protocol and memory model, we conducted model checking with a model of a mutator. In this wide range of case studies, we found faults in two GC algorithms, one of which is relevant to the memory model. We fixed these faults with the great help of counterexamples. We also modified some protocols so that they work under some memory models weaker than those for which the original protocols were designed, and checked them using model checking. We believe that bounded model checking is a feasible approach to investigate behavioral properties of concurrent copying protocols under weak memory models.
Effective interactive resolution of static analysis alarms
Authors: Zhang Xin , Grigore Radu , Si Xujie , Naik Mayur
Published: October 2017

We propose an interactive approach to resolve static analysis alarms. Our approach synergistically combines a sound but imprecise analysis with precise but unsound heuristics, through user interaction. In each iteration, it solves an optimization problem to find a set of questions for the user such that the expected payoff is maximized. We have implemented our approach in a tool, Ursa, that enables interactive alarm resolution for any analysis specified in the declarative logic programming language Datalog. We demonstrate the effectiveness of Ursa on a state-of-the-art static datarace analysis using a suite of 8 Java programs comprising 41-194 KLOC each. Ursa is able to eliminate 74% of the false alarms per benchmark with an average payoff of 12× per question. Moreover, Ursa prioritizes user effort effectively by posing questions that yield high payoffs earlier.
Natural synthesis of provably-correct data-structure manipulations
Authors: Qiu Xiaokang , Solar-Lezama Armando
Published: October 2017

This paper presents natural synthesis, which generalizes the proof-theoretic synthesis technique to support very expressive logic theories. This approach leverages the natural proof methodology and reduces an intractable, unbounded-size synthesis problem to a tractable, bounded-size synthesis problem, which is amenable to be handled by modern inductive synthesis engines. The synthesized program admits a natural proof and is a provably-correct solution to the original synthesis problem. We explore the natural synthesis approach in the domain of imperative data-structure manipulations and present a novel syntax-guided synthesizer based on natural synthesis. The input to our system is a program template together with a rich functional specification that the synthesized program must meet. Our system automatically produces a program implementation along with necessary proof artifacts, namely loop invariants and ranking functions, and guarantees the total correctness with a natural proof. Experiments show that our natural synthesizer can efficiently produce provably-correct implementations for sorted lists and binary search trees. To our knowledge, this is the first system that can automatically synthesize these programs, their functional correctness and their termination in tandem from bare-bones control flow skeletons.
Heaps don't lie: countering unsoundness with heap snapshots
Authors: Grech Neville , Fourtounis George , Francalanza Adrian , Smaragdakis Yannis
Published: October 2017

Static analyses aspire to explore all possible executions in order to achieve soundness. Yet, in practice, they fail to capture common dynamic behavior. Enhancing static analyses with dynamic information is a common pattern, with tools such as Tamiflex. Past approaches, however, miss significant portions of dynamic behavior, due to native code, unsupported features (e.g., invokedynamic or lambdas in Java), and more. We present techniques that substantially counteract the unsoundness of a static analysis, with virtually no intrusion to the analysis logic. Our approach is reified in the HeapDL toolchain and consists in taking whole-heap snapshots during program execution, that are further enriched to capture significant aspects of dynamic behavior, regardless of the causes of such behavior. The snapshots are then used as extra inputs to the static analysis. The approach exhibits both portability and significantly increased coverage. Heap information under one set of dynamic inputs allows a static analysis to cover many more behaviors under other inputs. A HeapDL-enhanced static analysis of the DaCapo benchmarks computes 99.5% (median) of the call-graph edges of unseen dynamic executions (vs. 76.9% for the Tamiflex tool).
Instrumentation bias for dynamic data race detection
Authors: Wood Benjamin P. , Cao Man , Bond Michael D. , Grossman Dan
Published: October 2017

This paper presents Fast Instrumentation Bias (FIB), a sound and complete dynamic data race detection algorithm that improves performance by reducing or eliminating the costs of analysis atomicity. In addition to checking for errors in target programs, dynamic data race detectors must introduce synchronization to guard against metadata races that may corrupt analysis state and compromise soundness or completeness. Pessimistic analysis synchronization can account for nontrivial performance overhead in a data race detector.

The core contribution of FIB is a novel cooperative ownership-based synchronization protocol whose states and transitions are derived purely from preexisting analysis metadata and logic in a standard data race detection algorithm. By exploiting work already done by the analysis, FIB ensures atomicity of dynamic analysis actions with zero additional time or space cost in the common case. Analysis of temporally thread-local or read-shared accesses completes safely with no synchronization. Uncommon write-sharing transitions require synchronous cross-thread coordination to ensure common cases may proceed synchronization-free.

We implemented FIB in the Jikes RVM Java virtual machine. Experimental evaluation shows that FIB eliminates nearly all instrumentation atomicity costs on programs where data often experience windows of thread-local access. Adaptive extensions to the ownership policy effectively eliminate high coordination costs of the core ownership protocol on programs with high rates of serialized sharing. FIB outperforms a naive pessimistic synchronization scheme by 50% on average. Compared to a tuned optimistic metadata synchronization scheme based on conventional fine-grained atomic compare-and-swap operations, FIB is competitive overall, and up to 17% faster on some programs. Overall, FIB effectively exploits latent analysis and program invariants to bring strong integrity guarantees to an otherwise unsynchronized data race detection algorithm at minimal cost.
Familia: unifying interfaces, type classes, and family polymorphism
Authors: Zhang Yizhou , Myers Andrew C.
Published: October 2017

Parametric polymorphism and inheritance are both important, extensively explored language mechanisms for providing code reuse and extensibility. But harmoniously integrating these apparently distinct mechanisms—and powerful recent forms of them, including type classes and family polymorphism—in a single language remains an elusive goal. In this paper, we show that a deep unification can be achieved by generalizing the semantics of interfaces and classes. The payoff is a significant increase in expressive power with little increase in programmer-visible complexity. Salient features of the new programming language include retroactive constraint modeling, underpinning both object-oriented programming and generic programming, and module-level inheritance with further-binding, allowing family polymorphism to be deployed at large scale. The resulting mechanism is syntactically light, and the more advanced features are transparent to the novice programmer. We describe the design of a programming language that incorporates this mechanism; using a core calculus, we show that the type system is sound. We demonstrate that this language is highly expressive by illustrating how to use it to implement highly extensible software and by showing that it can not only concisely model state-of-the-art features for code reuse, but also go beyond them.
FairSquare: probabilistic verification of program fairness
Authors: Albarghouthi Aws , D'Antoni Loris , Drews Samuel , Nori Aditya V.
Published: October 2017

With the range and sensitivity of algorithmic decisions expanding at a break-neck speed, it is imperative that we aggressively investigate fairness and bias in decision-making programs. First, we show that a number of recently proposed formal definitions of fairness can be encoded as probabilistic program properties. Second, with the goal of enabling rigorous reasoning about fairness, we design a novel technique for verifying probabilistic properties that admits a wide class of decision-making programs. Third, we present FairSquare, the first verification tool for automatically certifying that a program meets a given fairness property. We evaluate FairSquare on a range of decision-making programs. Our evaluation demonstrates FairSquare’s ability to verify fairness for a range of different programs, which we show are out-of-reach for state-of-the-art program analysis techniques.
Restricting grammars with tree automata
Authors: Adams Michael D. , Might Matthew
Published: October 2017

Precedence and associativity declarations in systems like yacc resolve ambiguities in context-free grammars (CFGs) by specifying restrictions on allowed parses. However, they are special purpose and do not handle the grammatical restrictions that language designers need in order to resolve ambiguities like dangling else, the interactions between binary operators and functional if expressions in ML, and the interactions between object allocation and function calls in JavaScript. Often, language designers resort to restructuring their grammars in order to encode these restrictions, but this obfuscates the designer's intent and can make grammars more difficult to read, write, and maintain.

In this paper, we show how tree automata can modularly and concisely encode such restrictions. We do this by reinterpreting CFGs as tree automata and then intersecting them with tree automata encoding the desired restrictions. The results are then reinterpreted back into CFGs that encode the specified restrictions. This process can be used as a preprocessing step before other CFG manipulations and is well behaved. It performs well in practice and never introduces ambiguities or LR(
k
) conflicts.
Understanding the use of lambda expressions in Java
Authors: Mazinanian Davood , Ketkar Ameya , Tsantalis Nikolaos , Dig Danny
Published: October 2017

Java 8 retrofitted lambda expressions, a core feature of functional programming, into a mainstream object-oriented language with an imperative paradigm. However, we do not know how Java developers have adapted to the functional style of thinking, and more importantly, what are the reasons motivating Java developers to adopt functional programming. Without such knowledge, researchers miss opportunities to improve the state of the art, tool builders use unrealistic assumptions, language designers fail to improve upon their designs, and developers are unable to explore efficient and effective use of lambdas.

We present the first large-scale, quantitative and qualitative empirical study to shed light on how imperative programmers use lambda expressions as a gateway into functional thinking. Particularly, we statically scrutinize the source code of 241 open-source projects with 19,770 contributors, to study the characteristics of 100,540 lambda expressions. Moreover, we investigate the historical trends and adoption rates of lambdas in the studied projects. To get a complementary perspective, we seek the underlying reasons on why developers introduce lambda expressions, by surveying 97 developers who are introducing lambdas in their projects, using the firehouse interview method.

Among others, our findings revealed an increasing trend in the adoption of lambdas in Java: in 2016, the ratio of lambdas introduced per added line of code increased by 54% compared to 2015. Lambdas were used for various reasons, including but not limited to (i) making existing code more succinct and readable, (ii) avoiding code duplication, and (iii) simulating lazy evaluation of functions. Interestingly, we found out that developers are using Java's built-in functional interfaces inefficiently, i.e., they prefer to use general functional interfaces over the specialized ones, overlooking the performance overheads that might be imposed. Furthermore, developers are not adopting techniques from functional programming, e.g., currying. Finally, we present the implications of our findings for researchers, tool builders, language designers, and developers.
Automated testing of graphics shader compilers
Authors: Donaldson Alastair F. , Evrard Hugues , Lascu Andrei , Thomson Paul
Published: October 2017

We present an automated technique for finding defects in compilers for graphics shading languages. key challenge in compiler testing is the lack of an oracle that classifies an output as correct or incorrect; this is particularly pertinent in graphics shader compilers where the output is a rendered image that is typically under-specified. Our method builds on recent successful techniques for compiler validation based on metamorphic testing, and leverages existing high-value graphics shaders to create sets of transformed shaders that should be semantically equivalent. Rendering mismatches are then indicative of shader compilation bugs. Deviant shaders are automatically minimized to identify, in each case, a minimal change to an original high-value shader that induces a shader compiler bug. We have implemented the approach as a tool, GLFuzz, targeting the OpenGL shading language, GLSL. Our experiments over a set of 17 GPU and driver configurations, spanning the main 7 GPU designers, have led to us finding and reporting more than 60 distinct bugs, covering all tested configurations. As well as defective rendering, these issues identify security-critical vulnerabilities that affect WebGL, including a significant remote information leak security bug where a malicious web page can capture the contents of other browser tabs, and a bug whereby visiting a malicious web page can lead to a ``blue screen of death'' under Windows 10. Our findings show that shader compiler defects are prevalent, and that metamorphic testing provides an effective means for detecting them automatically.
Bounded exhaustive test-input generation on GPUs
Authors: Celik Ahmet , Pai Sreepathi , Khurshid Sarfraz , Gligoric Milos
Published: October 2017

Bounded exhaustive testing is an effective methodology for detecting bugs in a wide range of applications. A well-known approach for bounded exhaustive testing is Korat. It generates all test inputs, up to a given small size, based on a formal specification that is written as an executable predicate and characterizes properties of desired inputs. Korat uses the predicate's executions on candidate inputs to implement a backtracking search based on pruning to systematically explore the space of all possible inputs and generate only those that satisfy the specification.

This paper presents a novel approach for speeding up test generation for bounded exhaustive testing using Korat. The novelty of our approach is two-fold. One, we introduce a new technique for writing the specification predicate based on an abstract representation of candidate inputs, so that the predicate executes directly on these abstract structures and each execution has a lower cost. Two, we use the abstract representation as the basis to define the first technique for utilizing GPUs for systematic test generation using executable predicates. Moreover, we present a suite of optimizations that enable effective utilization of the computational resources offered by modern GPUs. We use our prototype tool KoratG to experimentally evaluate our approach using a suite of 7 data structures that were used in prior studies on bounded exhaustive testing. Our results show that our abstract representation can speed up test generation by 5.68 times on a standard CPU, while execution on a GPU speeds up the execution, on average, by 17.46 times.
P/Taint: unified points-to and taint analysis
Authors: Grech Neville , Smaragdakis Yannis
Published: October 2017

Static information-flow analysis (especially taint-analysis) is a key technique in software security, computing where sensitive or untrusted data can propagate in a program. Points-to analysis is a fundamental static program analysis, computing what abstract objects a program expression may point to. In this work, we propose a deep unification of information-flow and points-to analysis. We observe that information-flow analysis is not a mere high-level client of points-to information, but it is indeed identical to points-to analysis on artificial abstract objects that represent different information sources. The very same algorithm can compute, simultaneously, two interlinked but separate results (points-to and information-flow values) with changes only to its initial conditions.

The benefits of such a unification are manifold. We can use existing points-to analysis implementations, with virtually no modification (only minor additions of extra logic for sanitization) to compute information flow concepts, such as value tainting. The algorithmic enhancements of points-to analysis (e.g., different flavors of context sensitivity) can be applied transparently to information-flow analysis. Heavy engineering work on points-to analysis (e.g., handling of the reflection API for Java) applies to information-flow analysis without extra effort. We demonstrate the benefits in a realistic implementation that leverages the Doop points-to analysis framework (including its context-sensitivity and reflection analysis features) to provide an information-flow analysis with excellent precision (over 91%) and recall (over 99%) for standard Java information-flow benchmarks.

The analysis comfortably scales to large, real-world Android applications, analyzing the Facebook Messenger app with more than 55
K
classes in under 7 hours.
Learning user friendly type-error messages
Authors: Wu Baijun , Campora III John Peter , Chen Sheng
Published: October 2017

Type inference is convenient by allowing programmers to elide type annotations, but this comes at the cost of often generating very confusing and opaque type error messages that are of little help to fix type errors. Though there have been many successful attempts at making type error messages better in the past thirty years, many classes of errors are still difficult to fix. In particular, current approaches still generate imprecise and uninformative error messages for type errors arising from errors in grouping constructs like parentheses and brackets. Worse, a recent study shows that these errors usually take more than 10 steps to fix and occur quite frequently (around 45% to 60% of all type errors) in programs written by students learning functional programming. We call this class of errors,
nonstructural errors
.

We solve this problem by developing Learnskell, a type error debugger that uses machine learning to help diagnose and deliver high quality error messages, for programs that contain nonstructural errors. While previous approaches usually report type errors on typing constraints or on the type level, Learnskell generates suggestions on the expression level. We have performed an evaluation on more than 1,500 type errors, and the result shows that Learnskell is quite precise. It can correctly capture 86% of all nonstructural errors and locate the error cause with a precision of 63%/87% with the first 1/3 messages, respectively. This is several times more than the precision of state-of-the-art compilers and debuggers. We have also studied the performance of Learnskell and found out that it scales to large programs.
Verifying strong eventual consistency in distributed systems
Authors: Gomes Victor B. F. , Kleppmann Martin , Mulligan Dominic P. , Beresford Alastair R.
Published: October 2017

Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly understood. Indeed, many published algorithms have later been shown to be incorrect, even some that were accompanied by supposed mechanised proofs of correctness. In this work, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data. We develop a modular and reusable framework in the Isabelle/HOL interactive proof assistant for verifying the correctness of CRDT algorithms. We avoid correctness issues that have dogged previous mechanised proofs in this area by including a network model in our formalisation, and proving that our theorems hold in all possible network behaviours. Our axiomatic network model is a standard abstraction that accurately reflects the behaviour of real-world computer networks. Moreover, we identify an abstract convergence theorem, a property of order relations, which provides a formal definition of strong eventual consistency. We then obtain the first machine-checked correctness theorems for three concrete CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement Counter. We find that our framework is highly reusable, developing proofs of correctness for the latter two CRDTs in a few hours and with relatively little CRDT-specific code.
Learning to blame: localizing novice type errors with data-driven diagnosis
Authors: Seidel Eric L. , Sibghat Huma , Chaudhuri Kamalika , Weimer Westley , Jhala Ranjit
Published: October 2017

Localizing type errors is challenging in languages with global type inference, as the type checker must make assumptions about what the programmer intended to do. We introduce Nate, a data-driven approach to error localization based on supervised learning. Nate analyzes a large corpus of training data -- pairs of ill-typed programs and their "fixed" versions -- to automatically learn a model of where the error is most likely to be found. Given a new ill-typed program, Nate executes the model to generate a list of potential blame assignments ranked by likelihood. We evaluate Nate by comparing its precision to the state of the art on a set of over 5,000 ill-typed OCaml programs drawn from two instances of an introductory programming course. We show that when the top-ranked blame assignment is considered, Nate's data-driven model is able to correctly predict the exact sub-expression that should be changed 72% of the time, 28 points higher than OCaml and 16 points higher than the state-of-the-art SHErrLoc tool. Furthermore, Nate's accuracy surpasses 85% when we consider the top two locations and reaches 91% if we consider the top three.
Paxos made EPR: decidable reasoning about distributed protocols
Authors: Padon Oded , Losa Giuliano , Sagiv Mooly , Shoham Sharon
Published: October 2017

Distributed protocols such as Paxos play an important role in many computer systems. Therefore, a bug in a distributed protocol may have tremendous effects. Accordingly, a lot of effort has been invested in verifying such protocols. However, checking invariants of such protocols is undecidable and hard in practice, as it requires reasoning about an unbounded number of nodes and messages. Moreover, protocol actions and invariants involve both quantifier alternations and higher-order concepts such as set cardinalities and arithmetic.

This paper makes a step towards automatic verification of such protocols. We aim at a technique that can verify correct protocols and identify bugs in incorrect protocols. To this end, we develop a methodology for deductive verification based on effectively propositional logic (EPR)—a decidable fragment of first-order logic (also known as the Bernays-Schönfinkel-Ramsey class). In addition to decidability, EPR also enjoys the finite model property, allowing to display violations as finite structures which are intuitive for users. Our methodology involves modeling protocols using general (uninterpreted) first-order logic, and then systematically transforming the model to obtain a model and an inductive invariant that are decidable to check. The steps of the transformations are also mechanically checked, ensuring the soundness of the method. We have used our methodology to verify the safety of Paxos, and several of its variants, including Multi-Paxos, Vertical Paxos, Fast Paxos, Flexible Paxos and Stoppable Paxos. To the best of our knowledge, this work is the first to verify these protocols using a decidable logic, and the first formal verification of Vertical Paxos, Fast Paxos and Stoppable Paxos.
Race, Law, and Health Disparities: Toward a Critical Race Intervention
Authors: Obasogie Osagie K. , Headen Irene , Mujahid Mahasin S.
Published: October 2017

In response to persistent and pervasive differences in health across racial and ethnic groups in the United States, there is a national commitment to achieving health equity, or optimal levels of health for all. Achieving health equity and eliminating health disparities is not without its challenges and will require interventions and approaches that focus on improving opportunity structures for racial/ethnic minorities. We provide a brief overview of the literature documenting black/white differences in health across the life course. We then discuss current conceptual models guiding this research and discuss the importance of translating legal theory—specifically, critical race approaches—to both the study of health disparities and the development of interventions to address them. We conclude with examples of research that incorporate, although not explicitly, aspects of critical race theory and discuss how this approach can be leveraged in future studies.
Judging the Judiciary by the Numbers: Empirical Research on Judges
Authors: Rachlinski Jeffrey J. , Wistrich Andrew J.
Published: October 2017

Do judges make decisions that are truly impartial? A wide range of experimental and field studies reveal that several extralegal factors influence judicial decision making. Demographic characteristics of judges and litigants affect judges' decisions. Judges also rely heavily on intuitive reasoning in deciding cases, making them vulnerable to the use of mental shortcuts that can lead to mistakes. Furthermore, judges sometimes rely on facts outside the record and rule more favorably toward litigants who are more sympathetic or with whom they share demographic characteristics. On the whole, judges are excellent decision makers and sometimes resist common errors of judgment that influence ordinary adults. The weight of the evidence, however, suggests that judges are vulnerable to systematic deviations from the ideal of judicial impartiality.
Impaired HLA Class I Antigen Processing and Presentation as a Mechanism of Acquired Resistance to Immune Checkpoint Inhibitors in Lung Cancer
Authors: Gettinger Scott , Choi Jungmin , Hastings Katherine , Truini Anna , Datar Ila , Sowell Ryan , Wurtz Anna , Dong Weilai , Cai Guoping , Melnick Mary Ann , Du Victor Y. , Schlessinger Joseph , Goldberg Sarah B. , Chiang Anne , Sanmamed Miguel F. , Melero Ignacio , Agorreta Jackeline , Montuenga Luis M. , Lifton Richard , Ferrone Soldano , Kavathas Paula , Rimm David L. , Kaech Susan M. , Schalper Kurt , Herbst Roy S. , Politi Katerina
Published: October 2017

Mechanisms of acquired resistance to immune checkpoint inhibitors (ICI) are poorly understood. We leveraged a collection of 14 ICI-resistant lung cancer samples to investigate whether alterations in genes encoding HLA Class I antigen processing and presentation machinery (APM) components or interferon signaling play a role in acquired resistance to PD-1 or PD-L1 antagonistic antibodies. Recurrent mutations or copy-number changes were not detected in our cohort. In one case, we found acquired homozygous loss of B2M that caused lack of cell-surface HLA Class I expression in the tumor and a matched patient-derived xenograft (PDX). Downregulation of B2M was also found in two additional PDXs established from ICI-resistant tumors. CRISPR-mediated knockout of B2m in an immunocompetent lung cancer mouse model conferred resistance to PD-1 blockade in vivo, proving its role in resistance to ICIs. These results indicate that HLA Class I APM disruption can mediate escape from ICIs in lung cancer.

Significance: As programmed death 1 axis inhibitors are becoming more established in standard treatment algorithms for diverse malignancies, acquired resistance to these therapies is increasingly being encountered. Here, we found that defective antigen processing and presentation can serve as a mechanism of such resistance in lung cancer. Cancer Discov; 7(12); 1420–35. ©2017 AACR.

This article is highlighted in the In This Issue feature, p. 1355
Consumptive Hypothyroidism: Case Report of Hepatic Hemangioendotheliomas Successfully Treated with Vincristine and Systematic Review of the Syndrome
Authors: Weber Pasa Marina , Scheffel Rafael Selbach , Borsatto Zanella André , Maia Ana Luiza , Dora José Miguel
Published: October 2017

Objectives: To provide a comprehensive description of consumptive hypothyroidism syndrome (CHS), a severe form of hypothyroidism that occurs due to the high expression levels of thyroid hormone inactivation enzyme type 3 deiodinase (D3) in tumors. Study Design: Case report and systematic review. Results: A 7-month-old girl with a diagnosis of massive hepatic hemangioendotheliomas was treated with high doses of thyroid hormones and tumor-directed chemotherapy with vincristine. The tumor displayed excellent response, and euthyroid status was regained. A systematic review on the databases PubMed/Medline and Embase was performed, using the term “Consumptive AND “Hypothyroidism.” From the 33 selected references, we extracted 42 case reports of CHS: 36 children and 6 adults. The laboratory profile at diagnosis displayed high TSH and low T4 and T3 serum levels. The serum reverse T3 and D3 activity levels were high in all patients tested. In children, 97% had vascular tumors, whereas in adults 33% were vascular tumors, 33% fibrous tumors, and 33% gastrointestinal stromal tumors. The conservative treatment was predominant in children, while in adults all cases were treated with surgery. Death occurred in 16% of children and 33% of adults. Conclusions: CHS is a rare form of hypothyroidism that occurs in children and adults, usually linked to hepatic vascular tumors. The condition is associated with high lethality. Prompt diagnosis, followed by high-dose thyroid hormone replacement and tumor-directed therapy are the keys to optimize outcomes.
Opposing Actions of AKT (Protein Kinase B) Isoforms in Vascular Smooth Muscle Injury and Therapeutic Response
Authors: Jin Yu , Xie Yi , Ostriker Allison C. , Zhang Xinbo , Liu Renjing , Lee Monica Y. , Leslie Kristen L. , Tang Waiho , Du Jing , Lee Seung Hee , Wang Yingdi , Sessa William C. , Hwa John , Yu Jun , Martin Kathleen A.
Published: October 2017

Objective—

Drug-eluting stent delivery of mTORC1 (mechanistic target of rapamycin complex 1) inhibitors is highly effective in preventing intimal hyperplasia after coronary revascularization, but adverse effects limit their use for systemic vascular disease. Understanding the mechanism of action may lead to new treatment strategies. We have shown that rapamycin promotes vascular smooth muscle cell differentiation in an AKT2-dependent manner in vitro. Here, we investigate the roles of AKT (protein kinase B) isoforms in intimal hyperplasia.

Approach and Results—

We found that germ-line–specific or smooth muscle–specific deletion of
Akt2
resulted in more severe intimal hyperplasia compared with control mice after arterial denudation injury. Conversely, smooth muscle–specific
Akt1
knockout prevented intimal hyperplasia, whereas germ-line
Akt1
deletion caused severe thrombosis. Notably, rapamycin prevented intimal hyperplasia in wild-type mice but had no therapeutic benefit in
Akt2
knockouts. We identified opposing roles for AKT1 and AKT2 isoforms in smooth muscle cell proliferation, migration, differentiation, and rapamycin response in vitro. Mechanistically, rapamycin induced
MYOCD
(myocardin) mRNA expression. This was mediated by AKT2 phosphorylation and nuclear exclusion of FOXO4 (forkhead box O4), inhibiting its binding to the
MYOCD
promoter.

Conclusions—

Our data reveal opposing roles for AKT isoforms in smooth muscle cell remodeling. AKT2 is required for rapamycin’s therapeutic inhibition of intimal hyperplasia, likely mediated in part through AKT2-specific regulation of MYOCD via FOXO4. Because AKT2 signaling is impaired in diabetes mellitus, this work has important implications for rapamycin therapy, particularly in diabetic patients.
Long-Term Potassium Monitoring and Dynamics in Heart Failure and Risk of Mortality
Authors: Núñez Julio , Bayés-Genís Antoni , Zannad Faiez , Rossignol Patrick , Núñez Eduardo , Bodí Vicent , Miñana Gema , Santas Enrique , Chorro Francisco J. , Mollar Anna , Carratalá Arturo , Navarro Jorge , Górriz Jose Luis , Lupón Josep , Husser Oliver , Metra Marco , Sanchis Juan
Published: October 2017

Background:

The prognostic value of long-term potassium monitoring and dynamics in heart failure has not been characterized completely. We sought to determine the association between serum potassium values collected at follow-up with all-cause mortality in a prospective and consecutive cohort of patients discharged from a previous acute heart failure admission.

Methods:

Serum potassium was measured at every physician-patient encounter, including hospital admissions and ambulatory settings. The multivariable-adjusted association of serum potassium with mortality was assessed by using comprehensive state-of-the-art regression methods that can accommodate time-dependent exposure modeling.

Results:

The study sample included 2164 patients with a total of 16 116 potassium observations. Mean potassium at discharge was 4.3±0.48 mEq/L. Hypokalemia (<3.5 mEq/L), normokalemia (3.5–5.0 mEq/L), and hyperkalemia (>5 mEq/L) were observed at the index admission in 77 (3.6%), 1965 (90.8%), and 122 (5.6%) patients, respectively. At a median follow-up of 2.8 years (range, 0.03–12.8 years), 1090 patients died (50.4%). On a continuous scale, the multivariable-adjusted association of potassium values and mortality revealed a nonlinear association (U-shaped) with higher risk at both ends of its distribution (omnibus
P
=0.001). Likewise, the adjusted hazard ratios for hypokalemia and hyperkalemia, normokalemia as reference, were 2.35 (95% confidence interval, 1.40–3.93;
P
=0.001) and 1.55 (95% confidence interval, 1.11–2.16;
P
=0.011), respectively (omnibus
P
=0.0003). Furthermore, dynamic changes in potassium were independently associated with substantial differences in mortality risk. Potassium normalization was independently associated with lower mortality risk (
P
=0.001).

Conclusions:

Either modeled continuously or categorically, serum potassium levels during long-term monitoring were independently associated with mortality in patients with heart failure. Likewise, persistence of abnormal potassium levels was linked to a higher risk of death in comparison with patients who maintained or returned to normal values.
New Data on Archaeobotany of the Lake Sevan Basin
Authors: Hovsepyan Roman
Published: October 2017

Recent archaeobotanical investigations (2013-2015) at three sites situated in the southeastern part of the Lake Sevan basin (Sotk-2, Norabak-1 and Sotk-1 settlements, and Sotk-10 cemetery) revealed important data on plant economy, agriculture, diet, and environment of the region during the Early Bronze Age, Middle-Late Bronze Age and Mediaeval periods. These materials show that agriculture was the main direction of plant economy to gain vegetal food staple, but it was likely accompanied also by gathering of wild plants. The principal direction of agriculture at the studied region was the cultivation of cereals for all the above-mentioned periods. Correspondingly, the main source of vegetal food were cereal-based products (presumably bread, porridges, etc).
Islamic Education and Personal Career Mobility in the Circassian Sultanate (Late 14th–Early 15th Century)
Authors: Zelenev Evgeny I. , Iliushina Milana
Published: October 2017

The authors explore the issue of education influence on the social status of people during the reign of the Circassian Sultans in Cairo (1382–1517). The study is focused on the issue, how social mobility, affected by the received education, could have influenced the personal status and the entire social structure of the Circassian Mamluks state.
Dialogues and Narratives Surrounding Confucius and His Disciples in the Shanghai Museum Manuscripts (上博楚簡有關孔子師徒的對話與故事)
Authors: Qiyong (郭齊勇) Guo
Published: October 2017

This article is a study of narratives and dialogues surrounding Confucius and his disciples in the Shanghai Museum Manuscripts, focusing on their relationship with received texts, as well as their periodization and genre division. The Shanghai Museum narratives seem to be situated between Lun yu (Analects) and Han Shi waizhuan (Han Ying’s Outer Commentary to the Poetry), in that they are not as succinct and precise as the former, but also not overly elaborate like the latter. These narratives are possibly the work of Confucians from the mid to late Warring States period.

通過討論上博簡中孔子與顔淵、子路、子貢等的對話或故事與經典的關係及其文字屬性問題,本文認爲其中有關內容,介於《論語》與《韓詩外傳》諸書之間,不如前者精煉、準確,又不像後者鋪陳太過。這可能就是戰國中後期的儒家作品。
Bureaus and Offices in Qin County-Level Administration (秦縣的列曹與諸官—— 從《洪範五行傳》一則佚文説起)
Authors: Wenbo (孫聞博) Sun
Published: October 2017

A prominent feature of Qin county-level administrative organization displayed in the newly unearthed Liye Qin slips is the division between bureaus (cao 曹) and offices (guan 官). On this point, fruitful comparison may be made with a recompiled excerpt from the lost Hongfan wuxing zhuan (Great Plan Five Phases Commentary), where government agencies are named according to the sexagenary ganzhi 干支 “heavenly stems and earthly branches” cycle. During the Qin period, bureaus were already established in commanderies and counties, however it would be inappropriate to classify all subordinate functionaries together as members of just “the arrayed bureaus” (liecao 列曹), as they were actually assigned to both bureaus and offices. Moreover, the role that Scribe (shi 史) personnel played in the operation of these bureaus and offices is also striking.

里耶秦簡所見縣級組織的突出特點是曹、官之分。這與《洪範五行傳》一則干支名官的佚文，可以對應。秦代郡縣已設曹，且郡、縣屬吏分類不宜以“列曹”統攝曹、官。而曹、官運作背後，引人注目的則是史類吏員的活躍。
The Military History of Qin and the Composition of Its Expeditionary Forces (秦國戰役史與遠征軍的構成)
Authors: Miyake (宮宅潔) Kiyoshi
Published: October 2017

From the late fourth century b.c.e. onward, the state of Qin launched several long-term military expeditions. If, however, the army had consisted of “alternating garrisons” (gengshu 更戍) serving a maximum enlistment of one year, such expeditions could not have been carried out. The author thereby argues that the term “surplus garrisons” (rongshu 冗戍) seen in the Liye Qin manuscripts designates long-term conscripts, with which Qin managed to sustain its long-term military operations.

公元前四世紀末期以後，秦國屢次進行長時段軍事遠征。如果兵士是以最長爲一年的任期而輪換的“更戍”，就不能完成這樣的軍事作戰。筆者推測，里耶秦簡所見“冗戍”是長期從軍的應徵兵。利用冗戍的兵力，秦國得以維持了長期軍事活動。
A Study of Sun Wu Seed Grain Loan Registers from Zoumalou (走馬樓吳簡中的種糧給貸簿研究)
Authors: Qu (熊曲) Xiong , Shaohua (宋少華) Song
Published: October 2017

This paper reconstructs two documents from the Three Kingdoms state of Wu unearthed at Zoumalou, Changsha, based on archaeological information as well as the form and contents of the excavated slips and tablets. The documents are registers of the state loaning seed grain to commoners: one type are “registers of grain loans,” while the other are “registers of seed grain loans from the Jiahe 3rd year.” Based on this reconstruction, we show that the standard unit to which the government loaned seed was the household, that the purpose was emergency relief of the poor, and that people received more grain than they needed for seed and were then able to eat some of it.

根據考古信息、簡牘形制及其內容，本文嘗試復原了走馬樓吳簡中的兩個官府種糧給貸簿書——出禾給貸簿和嘉禾三年種糧給貸簿。并由此認爲，官府借貸種糧以一户爲標準，以救濟貧民爲目的，但種糧的用途除了耕種外，也會用於口糧。