We propose a neurosymbolic architecture aimed at boosting the performance of any Language Model (LM) for SQL query generation. This approach leverages symbolic reasoning to guide the LM's exploration of the search space by considering multiple paths, symbolically evaluating choices at each decision point to choose the next step, with the added novel ability to backtrack. A key innovation is the use of symbolic checks on both partially and fully generated SQL queries, enabling early truncation of unsuccessful search paths. Input consists of textual requirements on the desired query, along with optional example tuples to be selected by the query. Experiments on Xander, our open-source implementation, show it both reduces runtime and increases accuracy of the generated SQL. A specific result is an LM using Xander outperforming a four-times-larger LM.

We establish a general framework for reasoning about the relationship between call-by-value and call-by-name. In languages with computational effects, call-by-value and call-by-name executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no effects, then whenever it terminates under call-by-value, it terminates with the same result under call-by-name. We propose a technique for stating and proving properties like these. The key ingredient is Levy's call-by-push-value calculus, which we use as a framework for reasoning about evaluation orders. We show that the call-by-value and call-by-name translations of expressions into call-by-push-value have related observable behaviour under certain conditions on computational effects, which we identify. We then use this fact to construct maps between the call-by-value and call-by-name interpretations of types, and identify further properties of effects that imply these maps form a Galois connection. These properties hold for some computational effects (such as divergence), but not others (such as mutable state). This gives rise to a general reasoning principle that relates call-by-value and call-by-name. We apply the reasoning principle to example computational effects including divergence and nondeterminism.

We establish a general framework for reasoning about the relationship between call-by-value and call-by-name. In languages with side-effects, call-by-value and call-by-name executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no side-effects, then whenever it terminates under call-by-value, it terminates with the same result under call-by-name. We propose a technique for stating and proving these properties. The key ingredient is Levy’s call-by-push-value calculus, which we use as a framework for reasoning about evaluation orders. We construct maps between the call-by-value and call-by-name interpretations of types. We then identify properties of side-effects that imply these maps form a Galois connection. These properties hold for some side-effects (such as divergence), but not others (such as mutable state). This gives rise to a general reasoning principle that relates call-by-value and call-by-name. We apply the reasoning principle to example side-effects including divergence and nondeterminism.

Dynamic analysis can identify improvements to programs that cannot feasibly be identified by static analysis; concurrency improvements are a motivating example. However, mapping these dynamic-analysis-based improvements back to patch-like source-code changes is non-trivial. We describe a system, Scopda, for generating source-code patches for improvements identified by execution-trace-based dynamic analysis. Scopda uses a graph-based static program representation (abstract program graph, APG), containing inter-procedural control flow and local data flow information, to analyse and transform static source-code. We demonstrate Scopda's ability to generate sensible source code patches for Java programs, though it is fundamentally language agnostic.

It is often difficult to analyse why a program executes more slowly than intended. This is particularly true for concurrent programs. We describe and evaluate a system, Rehype, which takes Java programs, performs low-overhead tracing of method calls, analyses the resulting trace-logs to detect inefficient uses of concurrency constructs, and suggests source-code-oriented improvements. Rehype deals with task-based concurrency, specifically a future-based model of tasks. Implementing the suggested improvements on an industrial API server more than doubled request-processing throughput.

Providing reliability is becoming a challenge for chip manufacturers, faced with simultaneously trying to improve miniaturization, performance and energy efficiency. This leads to very large margins on voltage and frequency, designed to avoid errors even in the worst case, along with significant hardware expenditure on eliminating voltage spikes and other forms of transient error, causing considerable inefficiency in power consumption and performance. We flip traditional ideas about reliability and performance around, by exploring the use of error resilience for power and performance gains. ParaMedic is a recent architecture that provides a solution for reliability with low overheads via automatic hardware error recovery. It works by splitting up checking onto many small cores in a heterogeneous multicore system with hardware logging support. However, its design is based on the idea that errors are exceptional. We transform ParaMedic into ParaDox, which shows high performance in both error-intensive and scarce-error scenarios, thus allowing correct execution even when undervolted and overclocked. Evaluation within error-intensive simulation environments confirms the error resilience of ParaDox and the low associated recovery cost. We estimate that compared to a non-resilient system with margins, ParaDox can reduce energy-delay product by 15% through undervolting, while completely recovering from any induced errors.

Execution tracing has an observer effect: the act of tracing perturbs program behaviour via its overhead, which can in turn affect the accuracy of subsequent dynamic analysis. We investigate this observer effect in the context of concurrent behaviour within JVM-based programs. Concurrent behaviour is especially fragile as task-scheduling ordering can change, which could even lead to deadlock via thread starvation under certain conditions. We analyse three dimensions of overhead, compute volume, memory volume, and uniformity, using a configurable-overhead tracer and a concurrency-performance analyser. We argue that uniformity is a key, and underappreciated, dimension of overhead that can have qualitative effects on program behaviour. Experimental results show that overhead significantly affects real-world concurrent behaviour and subsequent analysis, at times unintuitively.

In static analysis, two frameworks have been studied extensively: monotone data-flow analysis and type-and-effect systems. Whilst both are seen as general analysis frameworks, their relationship has remained unclear. Here we show that monotone data-flow analyses can be encoded as effect systems in a uniform way, via algebras of transfer functions. This helps to answer questions about the most appropriate structure for general effect algebras, especially with regards capturing control-flow precisely. Via the perspective of capturing data-flow analyses, we show the recent suggestion of using effect quantales is not general enough as it excludes non-distributive analyses e.g., constant propagation. By rephrasing the McCarthy transformation, we then model monotone data-flow effects via graded monads. This provides a model of data-flow analyses that can be used to reason about analysis correctness at the semantic level, and to embed data-flow analyses into type systems.

Computing precise (fully flow- and context-sensitive) and exhaustive (as against demand-driven) points-to information is known to be expensive. Top-down approaches require repeated analysis of a procedure for separate contexts. Bottom-up approaches need to model unknown pointees accessed indirectly through pointers that may be defined in the callers and hence do not scale while preserving precision. Therefore, most approaches to precise points-to analysis begin with a scalable but imprecise method and then seek to increase its precision. We take the opposite approach in that we begin with a precise method and increase its scalability. In a nutshell, we create naive but possibly non-scalable procedure summaries and then use novel optimizations to compact them while retaining their soundness and precision. For this purpose, we propose a novel abstraction called the generalized points-to graph (GPG), which views points-to relations as memory updates and generalizes them using the counts of indirection levels leaving the unknown pointees implicit. This allows us to construct GPGs as compact representations of bottom-up procedure summaries in terms of memory updates and control flow between them. Their compactness is ensured by strength reduction (which reduces the indirection levels), control flow minimization (which removes control flow edges while preserving soundness and precision), and call inlining (which enhances the opportunities of these optimizations). The effectiveness of GPGs lies in the fact that they discard as much control flow as possible without losing precision. This is the reason GPGs are very small even for main procedures that contain the effect of the entire program. This allows our implementation to scale to 158 kLoC for C programs. At a more general level, GPGs provide a convenient abstraction to represent and transform memory in the presence of pointers. Future investigations can try to combine it with other abstractions for static analyses that can benefit from points-to information.

Traditionally, reasoning about programs under varying evaluation regimes (call-by-value, call-by-name etc.) was done at the meta-level, treating them as term rewriting systems. Levy’s call-by-push-value (CBPV) calculus provides a more powerful approach for reasoning, by treating CBPV terms as a common intermediate language which captures both call-by-value and call-by-name, and by allowing equational reasoning about changes to evaluation order between or within programs. We extend CBPV to additionally deal with call-by-need, which is non-trivial because of shared reductions. This allows the equational reasoning to also support call-by-need. As an example, we then prove that call-by-need and call-by-name are equivalent if nontermination is the only side-effect in the source language. We then show how to incorporate an effect system. This enables us to exploit static knowledge of the potential effects of a given expression to augment equational reasoning; thus a program fragment might be invariant under change of evaluation regime only because of knowledge of its effects.

We present a type system combining subtyping and ML-style parametric polymorphism. Unlike previous work, our system supports type inference and has compact principal types. We demonstrate this system in the minimal language MLsub, which types a strict superset of core ML programs.

The notion of context in functional languages no longer refers just to variables in scope. Context can capture additional properties of variables (usage patterns in linear logics; caching requirements in dataflow languages) as well as additional resources or properties of the execution environment (rebindable resources; platform version in a cross-platform application). The recently introduced notion of coeffects captures the latter, whole-context properties, but it failed to capture fine-grained per-variable properties.

The problem of matching between binaries is important for software copyright enforcement as well as for identifying disclosed vulnerabilities in software. We present a search engine prototype called Rendezvous which enables indexing and searching for code in binary form. Rendezvous identifies binary code using a statistical model comprising instruction mnemonics, control flow sub-graphs and data constants which are simple to extract from a disassembly, yet normalising with respect to different compilers and optimisations. Experiments show that Rendezvous achieves F2measures of 86.7% and 83.0% on the GNU C library compiled with different compiler optimisations and the GNU coreutils suite compiled with gcc and clang respectively. These two code bases together comprise more than one million lines of code. Rendezvous will bring significant changes to the way patch management and copyright enforcement is currently performed.

We present a compositional approach to schedulability analysis of safety-critical Java programs. We introduce a specification language in order to write abstract behavioural specifications regarding task execution-time and use of resources. Schedulability is checked on a model composed of the abstract specifications, possibly before any implementation, and as the specifications are implemented, these implementations can be checked individually. This means that library routines potentially can be separately checked and reused, and individual tasks can be verified according to their specifications without performing the full-system-analysis.

Sequencing of effectful computations can be neatly captured using monads and elegantly written using do notation. In practice such monads often allow additional ways of composing computations, which have to be written explicitly using combinators.

Tracing algorithms visit reachable nodes in a graph and are central to activities such as garbage collection, marshalling etc. Traditional sequential algorithms use a worklist, replacing a nodes with their unvisited children. Previous work on parallel tracing is processor-oriented in associating one worklist per processor: worklist inser-tion and removal requires no locking, and load balancing requires only occasional locking. However, since multiple queues may con-tain the same node, significant locking is necessary to avoid con-current visits by competing processors. This paper presents a memory-oriented solution: memory is par-titioned into segments and each segment has its own worklist con-taining only nodes in that segment. At a given time at most one pro-cessor owns a given worklist. By arranging separate single-reader-single-writer forwarding queues to pass nodes from processor i to processor j we can process objects in an order that gives lock-free mainline code and improved locality of reference. This refactoring is analogous to the way in which a compiler changes an iteration space to eliminate data dependencies. While it is clear that our solution can be more effective on NUMA systems, and even necessary when processor-local memory may not be addressed from other processors, slightly surprisingly, it often gives significantly better speed-up on modern multi-cores architectures too. Using caches to hide memory latency loses much of its effectiveness when there is significant cross-processor mem-ory contention or when locking is necessary.

Thread-level speculation (TLS) is a technique that allows parts of a sequential program to be executed in parallel. TLS ensures the parallel program’s behaviour remains true to the language’s original sequential semantics; for example, allowing multiple iterations of a loop to run in parallel if there are no conflicts between them. Conventional software-TLS algorithms detect conflicts dynamically. They suffer from a number of problems. TLS implementations can impose large storage overheads caused by buffering speculative work. TLS implementations can offer disappointing scalability, if threads can only commit speculative work back to the “real ” heap sequentially. TLS implementations can be slow because speculative reads must consult look-aside tables to see earlier speculative writes, or because speculative operations replace normal reads and writes with expensive synchronisation primitives (e.g. CAS or memory fences). We present a streamlined software-TLS algorithm for mostlyparallel loops that aims to avoid these problems. We allow speculative work to be performed in place, so we avoid buffering, and so that reads naturally see earlier writes. We avoid needing a serialcommit protocol. We avoid the need for CAS or memory fences in common operations. We strive to reduce the size of TLS-related conflict-detection state, and to interact well with typical data-cache implementations. We evaluate our implementation on off-the-shelf hardware using seven applications from SciMark2, BYTEmark and JOlden. We achieve an average 77 % of the speed-up of manuallyparallelized versions of the benchmarks for fully parallel loops. We achieve a maximum of a 5.8x speed-up on an 8-core machine.

The growing popularity of hardware virtualization (VMware and Xen being two prominent implementations) leads us to examine the common ground between this yet-again vibrant technology and partial evaluation. A virtual machine executes on host hardware and presents to its guest program a replica of that host environment, complete with CPU, memory, and I/O devices. A virtual machine can be seen as a self-interpreter.

Our loop parallelizing method of compiler for SIMD architecture enables SIMD instructions to be generated from loops which include complicated data dependency. The characteristic of our method is in choosing the more optimising method for parallelization from two shearing conversions by inner and outer loop carried data dependences. One of them is novel and involves shearing horizontally along the inner loop index and the other is well-established shearing vertically along the outer loop index. These loop transformations are formalized by matrix operations. They enable the original loop indexes to be expressed using new loop indexes so that compiler does not need to make any change in loop body. At this point, simple templates suffice to generate optimal code. To conclude we summarize the conditions for choosing suitable shearing method and the requirements for conversion.

We have developed a bit-reversal algorithm (BRAVO) using vector permute operations, which is optimal in the number of permutations, and its cache-optimal version (COBRAVO). Our implementation on PowerMac G5 shows 2-4.5 fold improvement for small data sets and 15-75% improvement for large data sets (depending on the data element size) over the best known approach (COBRA).

Partial evaluation has been known for some time to be very effective when applied to software; in this paper we demonstrate that it can also be usefully applied to hardware. We present a bit-level algorithm that supports the offline partial evaluation of synchronous digital circuits. Full PE of combinational logic is noted to be equivalent to Boolean minimisation. A loop unrolling technique, supporting both partial and full unrolling, is described. Experimental results are given, showing that partial evaluation of a simple micro-processor against a ROM image is equivalent to compiling the ROM program directly into low level hardware.

We unify virtual-method despatch (polymorphism implementation) and network packet-routing operations; virtual-method calls correspond to network packets, and network addresses are allocated such that routing the packet corresponds to dispatching the call. As the run-time routing structure is inherent in network-on-chip platforms, this unification implements polymorphism for free.

Abstract We re-express Hudak and Young's higher-order strictness analysis for the untyped λ-calculus in a conceptually simpler and more semantically-based manner. We show our analysis to be a sound abstraction of Hudak and Young's which is also complete in a sense we make precise.

Traditionally, the theory of abstract interpretation has concentrated on the study of when one interpretation is sound (also safe or correct) with respect to another. We consider the dual notion of when one interpretation is complete with respect to another. Under the usual formulation of abstract interpretation, undecidability in general implies that a finitely computable sound abstraction of the standard interpretation is not complete. (For example, if we simplify 643 * (-192) to (+) * (-) using the “rule of signs” we cannot expect to retrieve -123456 from the resulting (1), even though we are certain that the result is negative.) Based on the idea that compilers can only depend on a finite number of program properties, we augment interpretations with predicate symbols specifying properties of interest (thereby replacing algebraic interpretations with logic interpretations). Interpretation J being sound (resp. complete) with respect to I is now phrased as “all questions (formulae) yielding true for J (resp. I) also yield true for I (resp. J)”.The traditional “rule of signs” turns out to be sound and complete for multiplication but only sound for addition.Sometimes abstract interpretations have spurious domain elements. The state minimisation algorithm for finite deterministic automata can be used to produce a canonical (simplest) abstract interpretation which is sound and complete with respect to any given finite abstract interpretation but possibly simpler to compute.A homomorphism always yields a sound and complete abstraction. Moreover, we show that a sound and complete abstraction map is not necessarily a homomorphism, but its composition with the natural map to the canonical interpretation is a homomorphism,One side-effect of our formulation of abstract interpretation is that it de-emphasises the ordering on the abstract domain which is relegated to an (optional) proof basis.

Data or program flow analysis is concerned with the static analysis of programs, to obtain as much information as possible about their possible run time behavior without actually having to run the programs. Due to the unsolvability of the halting problem (and nearly any other question concerning program behavior), such analyses are necessarily only approximate whenever the analysis algorithm is guaranteed to terminate. Further, exact analysis may be impossible due to the lack of knowledge of input data values, so the analysis can at best yield information about sets of possible computations.