arXiv subjects

Nick Palladinos

Publications and source records attributed to Nick Palladinos.

5 recordsLinked to original sources

arXiv2026

SAT Certificates for the Matrix-Multiplication Challenges over F2: All Ten `Expected-UNSAT` Instances Are Satisfiable, and a Type-3-Free Rank-23 Scheme

The matrix-multiplication SAT benchmark of Heule, Kauers, and Seidl asks, among other tasks, for solutions of ten known-satisfiable rank-23 formulas, proofs of unsatisfiability for ten formulas expected to be unsatisfiable, and a rank-23 scheme over $\mathbb{F}_2$ having a summand with no type-3 monomial. We give complete satisfying assignments for the 21 CNFs in the repository's top-level challenge1/, challenge2/, and challenge3/ directories at commit 150b2e2f. The principal finding is that all ten top-level Challenge-2 formulas are satisfiable. A direct audit shows that their hardcoded type-3 pairings are imposed by positive unit clauses on the 621 base variables: the formulas require selected incidences but do not forbid additional type-3 incidences. Starting from exact 23-summand schemes, we use the $\mathrm{GL}(3,2)^3$ isotropy action, cyclic trace symmetry, and perfect matching of transformed summands to constrained slots to construct witnesses for all ten files. For Challenge 3, we combine a locked semantic repair with a two-term identity over $\mathbb{F}_2$ to obtain a distinguished summand of type-3 count zero. Every semantic decomposition has zero residual in all 729 Brent equations. The accompanying DIMACS models assign all 26,541 variables of each formula and satisfy all 2,461,316 clauses across the 21 instances. A separate parser and clause evaluator rechecks the emitted models. A deterministic one-file Python reproducer regenerates the 21 certificates from the original CNFs in approximately nine seconds on the reported test host.

cs.SC↗

arXiv2024

Complete Fusion for Stateful Streams: Equational Theory of Stateful Streams and Fusion as Normalization-by-Evaluation

Processing large amounts of data fast, in constant and small space is the point of stream processing and the reason for its increasing use. Alas, the most performant, imperative processing code tends to be almost impossible to read, let alone modify, reuse -- or write correctly. We present both a stream compilation theory and its implementation as a portable stream processing library Strymonas that lets us assemble complex stream pipelines just by plugging in simple combinators, and yet attain the performance of hand-written imperative loops and state machines. The library supports finite and infinite streams and offers a rich set of combinators. They may be freely composed, and yet the resulting convoluted imperative code has no traces of combinator abstractions: no closures or intermediate objects. The high-performance is portable and statically guaranteed, without relying on compiler or black-box optimizations. We greatly exceed in performance the available stream processing libraries in OCaml. The library generates C and OCaml code. The declaratively built Strymonas pipelines are all stateful. The stream state introduced in the library is not directly observable. Therefore, the Strymonas API looks like the familiar interface of `pure functional' combinators. Programmers may introduce their own stream state and share it across the pipeline. Strymonas has been developed in tandem with the equational theory of stateful streams. Our theoretical model represents all desired pipelines and guarantees the existence of unique normal forms, which are mappable to (fused) state machines. We describe the normalization algorithm, as a form of normalization-by-evaluation. The equational theory lets us state and prove the correctness of the complete fusion optimization.

cs.PL↗

arXiv2022

Highest-performance Stream Processing

We present the stream processing library that achieves the highest performance of existing OCaml streaming libraries, attaining the speed and memory efficiency of hand-written state machines. It supports finite and infinite streams with the familiar declarative interface, of any combination of map, filter, take(while), drop(while), zip, flatmap combinators and tupling. Experienced users may use the lower-level interface of stateful streams and implement accumulating maps, compression and windowing. The library is based on assured code generation (at present, of OCaml and C) and guarantees in all cases complete fusion.

cs.PL↗

arXiv2016

Stream Fusion, to Completeness

Stream processing is mainstream (again): Widely-used stream libraries are now available for virtually all modern OO and functional languages, from Java to C# to Scala to OCaml to Haskell. Yet expressivity and performance are still lacking. For instance, the popular, well-optimized Java 8 streams do not support the zip operator and are still an order of magnitude slower than hand-written loops. We present the first approach that represents the full generality of stream processing and eliminates overheads, via the use of staging. It is based on an unusually rich semantic model of stream interaction. We support any combination of zipping, nesting (or flat-mapping), sub-ranging, filtering, mapping-of finite or infinite streams. Our model captures idiosyncrasies that a programmer uses in optimizing stream pipelines, such as rate differences and the choice of a "for" vs. "while" loops. Our approach delivers hand-written-like code, but automatically. It explicitly avoids the reliance on black-box optimizers and sufficiently-smart compilers, offering highest, guaranteed and portable performance. Our approach relies on high-level concepts that are then readily mapped into an implementation. Accordingly, we have two distinct implementations: an OCaml stream library, staged via MetaOCaml, and a Scala library for the JVM, staged via LMS. In both cases, we derive libraries richer and simultaneously many tens of times faster than past work. We greatly exceed in performance the standard stream libraries available in Java, Scala and OCaml, including the well-optimized Java 8 streams.

cs.PL↗

arXiv2014

Clash of the Lambdas

The introduction of lambdas in Java 8 completes the slate of statically-typed, mainstream languages with both object-oriented and functional features. The main motivation for lambdas in Java has been to facilitate stream-based declarative APIs, and, therefore, easier parallelism. In this paper, we evaluate the performance impact of lambda abstraction employed in stream processing, for a variety of high-level languages that run on a virtual machine (C#, F#, Java and Scala) and runtime platforms (JVM on Linux and Windows, .NET CLR for Windows, Mono for Linux). Furthermore, we evaluate the performance gain that two optimizing libraries (ScalaBlitz and LinqOptimizer) can offer for C#, F# and Scala. Our study is based on small-scale throughput-benchmarking, with significant care to isolate different factors, consult experts on the systems involved, and identify causes and opportunities. We find that Java exhibits high implementation maturity, which is a dominant factor in benchmarks. At the same time, optimizing frameworks can be highly effective for common query patterns.

cs.PL↗