Source-linked AI summary
An overview of Ciao and its design philosophy
M. V. Hermenegildo, F. Bueno, M. Carro, P. López-García, E. Mera, J. F. Morales, G. Puebla
TL;DR
Ciao addresses how a programming system can combine logic programming with features from multiple paradigms while retaining modular extensibility and practical development support. It presents a language and environment built around per-module features, assertions, analysis, verification, and optimization, reporting competitive compiled performance and integrated development capabilities. The paper is an informal overview intended to illustrate design philosophy rather than provide an exhaustive account.
Problem
Ciao seeks to combine logic programming, multiple programming paradigms, modular extensibility, and development support without sacrificing programmer flexibility or code quality.
Method
The paper presents Ciao’s per-module package system, assertion language, preprocessor, analysis, verification, compilation, and optimization mechanisms as an integrated programming environment.
Results
The optimizing compiler produced code competitive with strongly typed systems, while highly optimized compilation achieved a reported 7-fold speed-up relative to default bytecode in applications with tight memory and real-time constraints.
Takeaways & Limitations
Ciao supports selecting language features per module and combining interactive dynamic-language development with static analysis, verification, optimization, and automatic or manual parallelization.
Takeaways & Limitations
The current implementation still leaves a few builtins visible as of version 1.13.
Abstract
from arXiv · showhide
We provide an overall description of the Ciao multiparadigm programming system emphasizing some of the novel aspects and motivations behind its design and implementation. An important aspect of Ciao is that, in addition to supporting logic programming (and, in particular, Prolog), it provides the programmer with a large number of useful features from different programming paradigms and styles, and that the use of each of these features (including those of Prolog) can be turned on and off at will for each program module. Thus, a given module may be using, e.g., higher order functions and constraints, while another module may be using assignment, predicates, Prolog meta-programming, and concurrency. Furthermore, the language is designed to be extensible in a simple and modular way. Another important aspect of Ciao is its programming environment, which provides a powerful preprocessor (with an associated assertion language) capable of statically finding non-trivial bugs, verifying that programs comply with specifications, and performing many types of optimizations (including automatic parallelization). Such optimizations produce code that is highly competitive with other dynamic languages or, with the (experimental) optimizing compiler, even that of static languages, all while retaining the flexibility and interactive development of a dynamic language. This compilation architecture supports modularity and separate compilation throughout. The environment also includes a powerful auto-documenter and a unit testing framework, both closely integrated with the assertion system. The paper provides an informal overview of the language and program development environment. It aims at illustrating the design philosophy rather than at being exhaustive, which would be impossible in a single journal paper, pointing instead to previous Ciao literature.
1 Origins and Initial Motivations
Ciao combines a multiparadigm language with an extensible module system and an advanced development environment. Its design grew from parallel logic programming, program analysis, and the goal of improving programmer productivity while retaining dynamic-language flexibility and static-language performance.
- Ciao combines a multiparadigm programming language with an advanced environment aimed at helping programmers produce code with fewer bugs and less effort.
- The system architecture targets efficient execution across platforms from small embedded processors to powerful multicore architectures.
- Ciao’s design evolved from &-Prolog research on exploiting and-parallelism through specialized abstract machines, automatic annotation, and abstract-interpretation-based analysis.
- The assertion language and Ciao Preprocessor use inferred program information for cooperative static and dynamic verification, bug finding, specification checking, and optimization.
- Its kernel language and programmable packages let developers define syntax and semantics modularly, activating extensions independently for each compilation unit.Packages group syntactic definitions, compilation options, and compiler plugins.
2 Supporting Multiple Paradigms and Useful Features
Ciao supports multiple programming paradigms through modular packages that transform source-level extensions into a common kernel language. Features such as functional notation, higher-order programming, constraints, alternative computation rules, and Prolog compatibility can be selected per module.
- Extensible module system: Packages let Ciao combine multiple programming paradigms by compiling source-level sub-languages into a common kernel language.The kernel is essentially pure Prolog with additional instrumental functionality, while packages define syntax and source-to-source transformations.
- Extensible module system: Packages modify only the module where they are loaded, allowing different modules to use incompatible syntax and semantics without clashes.Packages can be loaded through module declarations or use package declarations.
- Functional and higher-order programming: Functional packages provide function-like notation, higher-order predicate abstractions, applications, and optional lazy evaluation.The functional extension uses flattening and resolution, with freeze/2 supporting lazy evaluation rather than narrowing.
- Functional and higher-order programming: The hiord package translates higher-order calls into call/N and supports predicate abstractions whose applications can produce transformed lists.For example, mapping an abstraction that computes f(X) over [1,3,2] produces [f(1),f(3),f(2)].
- Prolog and logic-programming variants: Ciao can provide classic and ISO-Prolog behavior through optional packages while also allowing modules restricted to pure logic programming.Classical Prolog code can run without modification through defaults, whereas omitting classic packages makes impure predicates such as assert/1 undefined.
- Prolog and logic-programming variants: Additional packages provide alternative computation rules, including breadth-first search, iterative deepening, tabling, and the Andorra model.These alternatives are made available by loading suitable packages.
3 Ciao Assertions
Ciao assertions provide a language for expressing program properties across calls, successes, computations, and program points. The system uses these assertions for checking, verification, testing, documentation, and analysis of partially developed code.
- Assertion language: Ciao assertions express preconditions, postconditions, whole-computation properties, and constraints at program points.The assertion language appears as an extended declaration syntax and includes pred assertions and program-point assertions.
- Assertion language: Pred assertions describe admissible call states, success states, and computational properties for particular predicates.Their general schema combines an optional precondition, postcondition, and computation-properties field.
- State properties: State properties used in assertions may be user-defined or imported, but they must be explicitly marked and terminate for every possible call.They can participate in both compile-time checking and runtime checks.
- Computational properties: Assertions can specify computation behavior such as nonfailure, determinacy, termination, and resolution-step complexity.One example describes a terminating functional computation, while another states that nrev/2 uses O(length(A)) resolution steps for list inputs.
- Assertion processing: Assertion status distinguishes programmer-provided checks and trusted information from analyzer-produced or verified assertions.Statuses include check, trust, true, checked, and false, representing different sources or verification outcomes.
- Uses of assertions: Assertions support testing, verification, and documentation, including descriptions of modules or classes that are not yet implemented or are written in other languages.This allows checkers, verifiers, and documenters to operate on partially developed code.
4 The Ciao Unified Assertion Framework
CiaoPP’s unified assertion framework uses assertions as a readable communication medium across verification and testing tools. It combines static analysis with assertion checking, supports safe handling of complex properties, and can feed analysis results into optimization.
- Framework architecture: CiaoPP’s architecture communicates information among verification and testing tools primarily through assertions, keeping intermediate results readable to users.The framework takes a user program and optional assertions as input, with tools connected by communication paths.
- Assertion checking: Compile-time checking compares static-analysis results with assertions to detect specification violations without relying solely on runtime checks.Static analysis typically uses abstract interpretation or another mechanism providing safe upper or lower approximations of relevant properties.
- Assertion checking: Safe approximations and an acceptable check status let CiaoPP handle complex assertions, including lower and upper bounds on procedure computational cost.The framework may verify or falsify efficiency assertions while retaining an intermediate check status when the comparison is inconclusive.
- Compilation integration: Assertion checking is module-aware, and analysis information can subsequently be used to optimize programs during compilation.The framework also supports analyses concerning execution-time bounds and user-defined resource consumption.
5 Static Verification, Debugging, Run-Time Checking, and Unit Testing in Practice
CiaoPP combines static analysis, verification, debugging, run-time assertion checks, and unit testing within a unified framework. The examples show it inferring resource properties, rejecting an incorrect complexity claim, locating a run-time sorting bug, and supporting a substantial ISO-Prolog test suite.
- 5.1 Automatic Inference of (Non-Trivial) Code Properties: CiaoPP infers modes, types, non-failure, term-size bounds, and computational-cost bounds from program analysis.Cost bounds are expressed as functions of input sizes; a finite upper cost bound also implies termination.
- 5.2 Static (Performance) Verification and Debugging: The analyzer detects that naive reverse requires a quadratic lower bound, contradicting a user assertion requiring O(length(A)) resolution steps.The inferred lower bound is 0.5*exp(length(A),2)+1.5*length(A)+1 resolution steps.
- 5.3 Run-Time Checking: CiaoPP translates unverifiable assertions into run-time checks that expose violations when a buggy qsort/2 returns an unsorted result.The checks report the violated sorted_num_list property and can identify the erroneous call through a more verbose call-stack dump.
- 5.3 Run-Time Checking: The call-stack output localizes the qsort/2 defect to swapped variables in a conc/3 call, while confirming that the returned list is ground.The reported outputs are reverse-sorted, indicating the R1 and R2 variables were exchanged.
- 5.4 Unit Testing: Ciao unit tests reuse the assertion language, and static checking can sometimes avoid executing tests while run-time checks and tests share infrastructure.The framework supported 976 tests for checking ISO-Prolog compliance in Ciao.
6 High Performance with Less Effort
Ciao combines inferred program information with assertions and analysis to reduce programmer effort while enabling optimization, including automatic parallelization. Its compilers can produce efficient code across dynamic-language and static-language settings, with specialized support for parallel execution and low-level performance.
- High Performance with Less Effort: Ciao infers program properties when users do not provide declarations, allowing the same kernel-level analyses to support multiple programming models.The inferred information is reused for optimization and development support.
- High Performance with Less Effort: Abstract-analysis information supports high-level optimizations such as specialization, partial evaluation, dead-code removal, goal reordering, and reduced concurrency or dynamic scheduling.
- High Performance with Less Effort: A 7-fold speed-up over default bytecode compilation was achieved for real-time spatial placement of sound sources on an embedded processor.The default bytecode performance was already similar to state-of-the-art abstract-machine systems.
- High Performance with Less Effort: ImProlog-generated code was on average 8% slower than the highly optimized YAP 5.1.2 emulator and 44% faster than the stock Ciao emulator.ImProlog combines type and mode assertions with imperative features such as low-level pointers and destructive assignment.
- High Performance with Less Effort: Automatic parallelization transforms source programs into parallel expressions while exploiting independence conditions intended to preserve correctness and avoid slowdown.The approach can parallelize manually written or compiler-generated code and supports programmer inspection of the resulting source-level parallelization.
- High Performance with Less Effort: Ciao uses POSIX-based threads and task stealing to support independent and-parallel execution while decoupling operating-system thread counts from parallel-goal counts.
7 Incremental Compilation and Other Support for Programming in the Small and in the Large
Ciao’s module system supports modular analysis, static debugging, incremental compilation, and optimization, while its deployment facilities span scripting, interpretation, compilation, and reduced-size executables.
- Incremental Compilation and Other Support for Programming in the Small and in the Large: The module system enables modular program development, global analysis, static debugging, and module-based incremental compilation and optimization.
- Incremental Compilation and Other Support for Programming in the Small and in the Large: Ciao supports interpreter, scripting-language, and compiled-language use, producing bytecode or standalone executables across multiple operating systems.
- Incremental Compilation and Other Support for Programming in the Small and in the Large: Modular analysis can generate stripped executables containing only the builtins and libraries used by an application.This supports programming under strict space constraints.
- Incremental Compilation and Other Support for Programming in the Small and in the Large: Assertions describe foreign interfaces to C/C++, Java, Tcl/Tk, and SQL databases, with glue code generated automatically.
8 An Advanced Integrated Development Environment
Ciao integrates interactive development tools with its preprocessor, debugger, documentation system, and assertion-based checking facilities. The environment supports direct inspection, transformation, documentation, and static error localization.
- An Advanced Integrated Development Environment: The graphical development interface provides direct access to the top level, debugger, preprocessor, autodocumenter, and related tools.
- An Advanced Integrated Development Environment: Debugging highlights the current program statement in the source buffer while tracing execution.
- An Advanced Integrated Development Environment: The environment offers documentation access, syntax highlighting, auto-completion, source error location, customization, and interactive control of static debugging and transformations.
- An Advanced Integrated Development Environment: CiaoPP statically detected that nrev violated an assertion requiring linear complexity.The system presents this cost-related semantic error in the source.
- An Advanced Integrated Development Environment: Assertions and program information can be converted into human-readable documentation in multiple formats on a per-module basis.
9 Some Final Thoughts: Dynamic vs. Static Languages, Parallelism
Ciao addresses the tension between dynamic-language flexibility and static-language checking through optional assertions, safe static analysis, and runtime checks. Its design also supports multiple paths to parallelism, allowing programmers to write, infer, inspect, and verify parallel code.
- Some Final Thoughts: Dynamic vs. Static Languages, Parallelism: Ciao targets dynamic scenarios while avoiding compulsory type and mode declarations that the authors felt could hinder programming in the small.
- Some Final Thoughts: Dynamic vs. Static Languages, Parallelism: The assertion methodology performs a best-effort static analysis using safe approximations while allowing runtime checks when complete verification is not possible.Assertions can describe properties beyond types, including modes, determinacy, non-failure, sharing, linearity, and cost.
- Some Final Thoughts: Dynamic vs. Static Languages, Parallelism: Ciao’s shared assertion framework supports static verification, runtime checking, unit testing, and documentation across a modular and extensible system.
- Some Final Thoughts: Dynamic vs. Static Languages, Parallelism: The paper presents Ciao as an approach to combining dynamic-language features with static-system performance and efficiency.
- Some Final Thoughts: Dynamic vs. Static Languages, Parallelism: Ciao supports manual parallelism, compiler-discovered parallelism, or a combination, while checking manual parallelizations and exposing generated source-level parallelizations for inspection.