Interval-based resource usage verification: Formalization and prototype

In an increasing number of applications (e.g., in embedded, real-time, or mobile systems) it is important or even essential to ensure conformance with respect to a specification expressing resource usages, such as execution time, memory, energy, or user-defined resources. In previous work we have presented a novel framework for data size-aware, static resource usage verification. Specifications can include both lower and upper bound resource usage functions. In order to statically check such specifications, both upper- and lower-bound resource usage functions (on input data sizes) approximating the actual resource usage of the program which are automatically inferred and compared against the specification. The outcome of the static checking of assertions can express intervals for the input data sizes such that a given specification can be proved for some intervals but disproved for others. After an overview of the approach in this paper we provide a number of novel contributions: we present a full formalization, and we report on and provide results from an implementation within the Ciao/CiaoPP framework (which provides a general, unified platform for static and run-time verification, as well as unit testing). We also generalize the checking of assertions to allow preconditions expressing intervals within which the input data size of a program is supposed to lie (i.e., intervals for which each assertion is applicable), and we extend the class of resource usage functions that can be checked.

An overview of the ciao multiparadigm language and program development environment and its design philosophy

We describe some of the novel aspects and motivations behind the design and implementation of the Ciao multiparadigm programming system. An important aspect of Ciao is that 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 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 objects, predicates, 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 program optimizations. Such optimizations produce code that is highly competitive with other dynamic languages or, when the highest levéis of optimization are used, even that of static languages, all while retaining the interactive development environment of a dynamic language. The environment also includes a powerful auto-documenter. 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 the format of a paper, pointing instead to the existing literature on the system.

An abstract interpretation-based approach to mobile code safety

Recent approaches to mobile code safety, like proof- arrying code, involve associating safety information to programs. The code supplier provides a program and also includes with it a certifícate (or proof) whose validity entails compliance with a predefined safety policy. The intended benefit is that the program consumer can locally validate the certifícate w.r.t. the "untrusted" program by means of a certifícate checker—a process which should be much simpler, eflicient, and automatic than generating the original proof. We herein introduce a novel approach to mobile code safety which follows a similar scheme, but which is based throughout on the use of abstract interpretation techniques. In our framework the safety policy is specified by using an expressive assertion language defined over abstract domains. We identify a particular slice of the abstract interpretation-based static analysis results which is especially useful as a certifícate. We propose an algorithm for checking the validity of the certifícate on the consumer side which is itself in fact a very simplified and eflicient specialized abstract-interpreter. Our ideas are illustrated through an example implemented in the CiaoPP system. Though further experimentation is still required, we believe the proposed approach is of interest for bringing the automation and expressiveness which is inherent in the abstract interpretation techniques to the área of mobile code safety.

A system for automatically generating documentation for (C)LP programs

We describe lpdoc, a tool which generates documentation manuals automatically from one or more logic program source files, written in ISO-Prolog, Ciao, and other (C)LP languages. It is particularly useful for documenting library modules, for which it automatically generates a rich description of the module interface. However, it can also be used quite successfully to document full applications. A fundamental advantage of using lpdoc is that it helps maintaining a true correspondence between the program and its documentation, and also identifying precisely to what version of the program a given printed manual corresponds. The quality of the documentation generated can be greatly enhanced by including within the program text assertions (declarations with types, modes, etc.) for the predicates in the program, and machine-readable comments. One of the main novelties of lpdoc is that these assertions and comments are written using the Ciao system assertion language, which is also the language of communication between the compiler and the user and between the components of the compiler. This allows a significant synergy among specification, documentation, optimization, etc. A simple compatibility library allows conventional (C)LP systems to ignore these assertions and comments and treat normally programs documented in this way. The documentation can be generated in many formats including texinfo, dvi, ps, pdf, info, html/css, Unix nroff/man, Windows help, etc., and can include bibliographic citations and images. lpdoc can also generate “man” pages (Unix man page format), nicely formatted plain ascii “readme” files, installation scripts useful when the manuals are included in software distributions, brief descriptions in html/css or info formats suitable for inclusion in on-line indices of manuals, and even complete WWW and info sites containing on-line catalogs of documents and software distributions. The lpdoc manual, all other Ciao system manuals, and parts of this paper are generated by lpdoc.

A documentation generator for logic programming systems

We describe lpdoc, a tool which generates documentation manuals automatically from one or more logic program source files, written in ISO-Prolog, Ciao, and other (C)LP languages. It is particularly useful for documenting library modules, for which it automatically generates a rich description of the module interface. However, it can also be used quite successfully to document full applications. The documentation can be generated in many formats including t e x i n f o, dvi, ps, pdf, inf o, html/css, Unix nrof f/man, Windows help, etc., and can include bibliographic citations and images, lpdoc can also genérate "man" pages (Unix man page format), nicely formatted plain ascii "readme" files, installation scripts useful when the manuals are included in software distributions, brief descriptions in html/css or inf o formats suitable for inclusión in on-line Índices of manuals, and even complete WWW and inf o sites containing on-line catalogs of documents and software distributions. A fundamental advantage of using lpdoc is that it helps maintaining a true correspondence between the program and its documentation, and also identifying precisely to what versión of the program a given printed manual corresponds. The quality of the documentation generated can be greatly enhanced by including within the program text assertions (declarations with types, modes, etc. ...) for the predicates in the program, and machine-readable comments. These assertions and comments are written using the Ciao system assertion language. A simple compatibility library allows conventional (C)LP systems to ignore these assertions and comments and treat normally programs documented in this way. The lpdoc manual, all other Ciao system manuals, and most of this paper, are generated by lpdoc.

An overview of ciao and its design philosophy

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 autodocumenter 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.

Resource bounds analysis.

We present a generic analysis that infers both upper and lower bounds on the usage that a program makes of a set of user-definable resources. The inferred bounds will in general be functions of input data sizes. A resource in our approach is a quite general, user-defined notion which associates a basic cost function with elementary operations. The analysis then derives the related (upper- and lower- bound) cost functions for all procedures in the program. We also present an assertion language which is used to define both such resources and resource-related properties that the system can then check based on the results of the analysis. We have performed some experiments with some concrete resource-related properties such as execution steps, bits sent or received by an application, number of arithmetic operations performed, number of calls to a procedure, number of transactions, etc. presenting the resource usage functions inferred and the times taken to perform the analysis. Applications of our analysis include resource consumption verification and debugging (including for mobile code), resource control in parallel/distributed computing, and resource-oriented specialization.

The ciao prolog system

Ciao is a public domain, next generation multi-paradigm programming environment with a unique set of features: Ciao offers a complete Prolog system, supporting ISO-Prolog, but its novel modular design allows both restricting and extending the language. As a result, it allows working with fully declarative subsets of Prolog and also to extend these subsets (or ISO-Prolog) both syntactically and semantically. Most importantly, these restrictions and extensions can be activated separately on each program module so that several extensions can coexist in the same application for different modules. Ciao also supports (through such extensions) programming with functions, higher-order (with predicate abstractions), constraints, and objects, as well as feature terms (records), persistence, several control rules (breadth-first search, iterative deepening, ...), concurrency (threads/engines), a good base for distributed execution (agents), and parallel execution. Libraries also support WWW programming, sockets, external interfaces (C, Java, TclTk, relational databases, etc.), etc. Ciao offers support for programming in the large with a robust module/object system, module-based separate/incremental compilation (automatically -no need for makefiles), an assertion language for declaring (optional) program properties (including types and modes, but also determinacy, non-failure, cost, etc.), automatic static inference and static/dynamic checking of such assertions, etc. Ciao also offers support for programming in the small producing small executables (including only those builtins used by the program) and support for writing scripts in Prolog. The Ciao programming environment includes a classical top-level and a rich emacs interface with an embeddable source-level debugger and a number of execution visualization tools. The Ciao compiler (which can be run outside the top level shell) generates several forms of architecture-independent and stand-alone executables, which run with speed, efficiency and executable size which are very competive with other commercial and academic Prolog/CLP systems. Library modules can be compiled into compact bytecode or C source files, and linked statically, dynamically, or autoloaded. The novel modular design of Ciao enables, in addition to modular program development, effective global program analysis and static debugging and optimization via source to source program transformation. These tasks are performed by the Ciao preprocessor ( ciaopp, distributed separately). The Ciao programming environment also includes lpdoc, an automatic documentation generator for LP/CLP programs. It processes Prolog files adorned with (Ciao) assertions and machine-readable comments and generates manuals in many formats including postscript, pdf, texinfo, info, HTML, man, etc. , as well as on-line help, ascii README files, entries for indices of manuals (info, WWW, ...), and maintains WWW distribution sites.

An automatic documentation generator for (C)LP - Reference manual

Lpdoc is an automatic program documentation generator for (C)LP systems. Lpdoc generates a reference manual automatically from one or more source files for a logic program (including ISO-Prolog, Ciao, many CLP systems, ...). It is particularly useful for documenting library modules, for which it automatically generates a description of the module interface. However, lpdoc can also be used quite successfully to document full applications and to generate nicely formatted plain ascii "readme" files. A fundamental advantage of using lpdoc to document programs is that it is much easier to maintain a true correspondence between the program and its documentation, and to identify precisely to what version of the program a given printed manual corresponds. The quality of the documentation generated can be greatly enhanced by including within the program text: • assertions (types, modes, etc. ...) for the predicates in the program, and • machine-readable comments (in the "literate programming" style). The assertions and comments included in the source file need to be written using the Ciao system assertion language. A simple compatibility library is available to make traditional (constraint) logic programming systems ignore these assertions and comments allowing normal treatment of programs documented in this way. The documentation is currently generated in HTML or texinf o format. From the texinf o output, printed and on-line manuals in several formats (dvi, ps, info, etc.) can be easily generated automatically, using publicly available tools, lpdoc can also generate 'man' pages (Unix man page format) as well as brief descriptions in html or emacs info formats suitable for inclusion in an on-line index of applications. In particular, lpdoc can create and maintain fully automatically WWW and info sites containing on-line versions of the documents it produces. The lpdoc manual (and the Ciao system manuals) are generated by lpdoc. Lpdoc is distributed under the GNU general public license. Note: lpdoc is fully supported on Linux, Mac OS X, and other Un*x-like systems. Due to the use of several Un*x-related utilities, some documentation back-ends may require Cygwin under Win32. This documentation corresponds to version 3.0 (2011/7/7, 16:33:15 CEST).

An ecological approach to anomaly detection: the EIA Model.

The presented work proposes a new approach for anomaly detection. This approach is based on changes in a population of evolving agents under stress. If conditions are appropriate, changes in the population (modeled by the bioindicators) are representative of the alterations to the environment. This approach, based on an ecological view, improves functionally traditional approaches to the detection of anomalies. To verify this assertion, experiments based on Network Intrussion Detection Systems are presented. The results are compared with the behaviour of other bioinspired approaches and machine learning techniques.

Subcellular localization of acetyl-CoA carboxylase in the apicomplexan parasite Toxoplasma gondii

Apicomplexan parasites such as Toxoplasma gondii contain a primitive plastid, the apicoplast, whose genome consists of a 35-kb circular DNA related to the plastid DNA of plants. Plants synthesize fatty acids in their plastids. The first committed step in fatty acid synthesis is catalyzed by acetyl-CoA carboxylase (ACC). This enzyme is encoded in the nucleus, synthesized in the cytosol, and transported into the plastid. In the present work, two genes encoding ACC from T. gondii were cloned and the gene structure was determined. Both ORFs encode multidomain proteins, each with an N-terminal extension, compared with the cytosolic ACCs from plants. The N-terminal extension of one isozyme, ACC1, was shown to target green fluorescent protein to the apicoplast of T. gondii. In addition, the apicoplast contains a biotinylated protein, consistent with the assertion that ACC1 is localized there. The second ACC in T. gondii appears to be cytosolic. T. gondii mitochondria also contain a biotinylated protein, probably pyruvate carboxylase. These results confirm the essential nature of the apicoplast and explain the inhibition of parasite growth in cultured cells by herbicides targeting ACC.

Ecological chaos in the wake of invasion.

Irregularities in observed population densities have traditionally been attributed to discretization of the underlying dynamics. We propose an alternative explanation by demonstrating the evolution of spatiotemporal chaos in reaction-diffusion models for predator-prey interactions. The chaos is generated naturally in the wake of invasive waves of predators. We discuss in detail the mechanism by which the chaos is generated. By considering a mathematical caricature of the predator-prey models, we go on to explain the dynamical origin of the irregular behavior and to justify our assertion that the behavior we present is a genuine example of spatiotemporal chaos.

The Hybrid Spirit Animating Chinese Pentecostals in Malaysia

This dissertation interrogates the assertion in postcolonial scholarship, especially from the work of Homi Bhabha that the construction and performance of hybrid identities act as a form of resistance for marginalized communities against structures of oppression. While this study supports this assertion, it also critiques how hybridity fails to address issues of unequal power relations. This has led to an uncritical use of hybridity that reproduces the very idea of static identity which its proponents claim to transcend. Through qualitative study of Chinese members of a Pentecostal church in Malaysia, this study argues that church members engage in "unequal belonging" where they privilege certain elements of their identities over others. In concert with Pierre Bourdieu's conceptions of habitus, field, and capital, unequal belonging highlights how hybridity fails to capture the intersecting and competing loyalties, strategies, and complexities of identity formation on a contextual level. Unequal belonging challenges postcolonial scholars to locate the subtle workings of power and privilege that manifest even among marginalized communities. The study first situates the Chinese through an analysis of the historical legacy of British colonialism that has structured the country's current socio-political configuration along bounded categories of identification. The habitus constrains church members to accept certain Chinese ethnic markers as "givens." Although they face continuous marginalization, interviewee data demonstrates that church members negotiate their Chineseness and construct a "Modern Chinese" ethnic identity as a strategic move away from Chinese stereotypes. Moreover, conversion to Christianity affords church members access to cultural capital. Yet, it is limited and unequal capital. In particular, the "Chinese Chinese," who church members have demarcated as backward and traditional, are unable to gain access to this capital because they lack fluency in English and knowledge in modern, westernized worldviews. Unequal belonging nuances monolithic conceptions of hybridity. It demonstrates how church members' privilege of Christianity over Chineseness exposes the complex processes of power and privilege that makes westernized-English-speaking Chinese Christians culturally "higher" than non-English-speaking, non-Christian, Chinese. This study provides significant contribution to the complex aspect of hybridity where it is both a site of resistance and oppression.

Management of Trihalomethanes in Finished Drinking Water Through Source Water Precursor Monitoring

Trihalomethanes are organic compounds formed in drinking water distribution systems as a result of disinfection. This capstone project researched and evaluated the statistical correlation of trihalomethanes in finished drinking water and total organic carbon in source water using data generated by Denver area utilities. Results of the study conclude that some drinking water supply systems show a slight correlation between source water total organic carbon levels and trihalomethane levels in finished water. Results of the study also verify the assertion that changes to treatment for the reduction of trihalomethanes, for the protection of human health under the Safe Drinking Water Act should be determined by each utility, using information from gathered data, seasonal trends, and small scale batch testing.

The circumstellar environment and evolutionary status of the supergiant B[e] star Wd1-9

Context. Historically, supergiant (sg)B[e] stars have been difficult to include in theoretical schemes for the evolution of massive OB stars. Aims. The location of Wd1-9 within the coeval starburst cluster Westerlund 1 means that it may be placed into a proper evolutionary context and we therefore aim to utilise a comprehensive multiwavelength dataset to determine its physical properties and consequently its relation to other sgB[e] stars and the global population of massive evolved stars within Wd1. Methods. Multi-epoch R- and I-band VLT/UVES and VLT/FORS2 spectra are used to constrain the properties of the circumstellar gas, while an ISO-SWS spectrum covering 2.45−45μm is used to investigate the distribution, geometry and composition of the dust via a semi-analytic irradiated disk model. Radio emission enables a long term mass-loss history to be determined, while X-ray observations reveal the physical nature of high energy processes within the system. Results. Wd1-9 exhibits the rich optical emission line spectrum that is characteristic of sgB[e] stars. Likewise its mid-IR spectrum resembles those of the LMC sgB[e] stars R66 and 126, revealing the presence of equatorially concentrated silicate dust, with a mass of ~10−4M⊙. Extreme historical and ongoing mass loss (≳ 10−4M⊙yr−1) is inferred from the radio observations. The X-ray properties of Wd1-9 imply the presence of high temperature plasma within the system and are directly comparable to a number of confirmed short-period colliding wind binaries within Wd1. Conclusions. The most complete explanation for the observational properties of Wd1-9 is that it is a massive interacting binary currently undergoing, or recently exited from, rapid Roche-lobe overflow, supporting the hypothesis that binarity mediates the formation of (a subset of) sgB[e] stars. The mass loss rate of Wd1-9 is consistent with such an assertion, while viable progenitor and descendent systems are present within Wd1 and comparable sgB[e] binaries have been identified in the Galaxy. Moreover, the rarity of sgB[e] stars - only two examples are identified from a census of ~ 68 young massive Galactic clusters and associations containing ~ 600 post-Main Sequence stars - is explicable given the rapidity (~ 104yr) expected for this phase of massive binary evolution.