CSim 2

2021 ◽  
Vol 43 (1) ◽  
pp. 1-46
Author(s):  
David Sanan ◽  
Yongwang Zhao ◽  
Shang-Wei Lin ◽  
Liu Yang
Keyword(s):  
Programming Languages ◽  
Concurrent Systems ◽  
Theorem Prover ◽  
Compositional Techniques ◽  
Machine Code ◽  
Top Down ◽  
Hol Theorem Prover ◽  
High Level ◽  
High Degree

To make feasible and scalable the verification of large and complex concurrent systems, it is necessary the use of compositional techniques even at the highest abstraction layers. When focusing on the lowest software abstraction layers, such as the implementation or the machine code, the high level of detail of those layers makes the direct verification of properties very difficult and expensive. It is therefore essential to use techniques allowing to simplify the verification on these layers. One technique to tackle this challenge is top-down verification where by means of simulation properties verified on top layers (representing abstract specifications of a system) are propagated down to the lowest layers (that are an implementation of the top layers). There is no need to say that simulation of concurrent systems implies a greater level of complexity, and having compositional techniques to check simulation between layers is also desirable when seeking for both feasibility and scalability of the refinement verification. In this article, we present CSim 2 a (compositional) rely-guarantee-based framework for the top-down verification of complex concurrent systems in the Isabelle/HOL theorem prover. CSim 2 uses CSimpl, a language with a high degree of expressiveness designed for the specification of concurrent programs. Thanks to its expressibility, CSimpl is able to model many of the features found in real world programming languages like exceptions, assertions, and procedures. CSim 2 provides a framework for the verification of rely-guarantee properties to compositionally reason on CSimpl specifications. Focusing on top-down verification, CSim 2 provides a simulation-based framework for the preservation of CSimpl rely-guarantee properties from specifications to implementations. By using the simulation framework, properties proven on the top layers (abstract specifications) are compositionally propagated down to the lowest layers (source or machine code) in each concurrent component of the system. Finally, we show the usability of CSim 2 by running a case study over two CSimpl specifications of an Arinc-653 communication service. In this case study, we prove a complex property on a specification, and we use CSim 2 to preserve the property on lower abstraction layers.

scholarly journals Workload Decomposition Strategies for Shared Memory Parallel Systems with OpenMP

2001 ◽  
Vol 9 (2-3) ◽  
pp. 109-122 ◽  
Author(s):  
Beniamino Di Martino ◽  
Sergio Briguglio ◽  
Gregorio Vlad ◽  
Giuliana Fogaccia
Keyword(s):  
Programming Languages ◽  
Parallel Programming ◽  
Shared Memory ◽  
Memory Systems ◽  
Particle In Cell ◽  
Decomposition Strategies ◽  
Programming Effort ◽  
High Level ◽  
Memory Architectures

A crucial issue in parallel programming (both for distributed and shared memory architectures) is work decomposition. Work decomposition task can be accomplished without large programming effort with use of high-level parallel programming languages, such as OpenMP. Anyway particular care must still be payed on achieving performance goals. In this paper we introduce and compare two decomposition strategies, in the framework of shared memory systems, as applied to a case study particle in cell application. A number of different implementations of them, based on the OpenMP language, are discussed with regard to time efficiency, memory occupancy, and program restructuring effort.

scholarly journals The verified CakeML compiler backend

2019 ◽  
Vol 29 ◽  
Author(s):  
YONG KIAM TAN ◽  
MAGNUS O. MYREEN ◽  
RAMANA KUMAR ◽  
ANTHONY FOX ◽  
SCOTT OWENS ◽  
...  
Keyword(s):  
Functional Programming ◽  
Theorem Prover ◽  
Runtime System ◽  
Machine Code ◽  
Garbage Collector ◽  
Overall Design ◽  
Data Representations ◽  
Arbitrary Precision ◽  
High Level ◽  
Intermediate Languages

AbstractThe CakeML compiler is, to the best of our knowledge, the most realistic verified compiler for a functional programming language to date. The architecture of the compiler, a sequence of intermediate languages through which high-level features are compiled away incrementally, enables verification of each compilation pass at an appropriate level of semantic detail. Parts of the compiler’s implementation resemble mainstream (unverified) compilers for strict functional languages, and it supports several important features and optimisations. These include efficient curried multi-argument functions, configurable data representations, efficient exceptions, register allocation, and more. The compiler produces machine code for five architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V. The generated machine code contains the verified runtime system which includes a verified generational copying garbage collector and a verified arbitrary precision arithmetic (bignum) library. In this paper, we present the overall design of the compiler backend, including its 12 intermediate languages. We explain how the semantics and proofs fit together and provide detail on how the compiler has been bootstrapped inside the logic of a theorem prover. The entire development has been carried out within the HOL4 theorem prover.

scholarly journals Implementing type theory in higher order constraint logic programming

2019 ◽  
Vol 29 (8) ◽  
pp. 1125-1150
Author(s):  
FERRUCCIO GUIDI ◽  
CLAUDIO SACERDOTI COEN ◽  
ENRICO TASSI
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Type System ◽  
Theorem Prover ◽  
Type Checking ◽  
Language Extension ◽  
Order Constraint ◽  
Simple Implementation ◽  
Calculus Of Inductive Constructions ◽  
High Level

In this paper, we are interested in high-level programming languages to implement the core components of an interactive theorem prover for a dependently typed language: the kernel – responsible for type-checking closed terms – and the elaborator – that manipulates open terms, that is terms containing unresolved unification variables.In this paper, we confirm that λProlog, the language developed by Miller and Nadathur since the 80s, is extremely suitable for implementing the kernel. Indeed, we easily obtain a type checker for the Calculus of Inductive Constructions (CIC). Even more, we do so in an incremental way by escalating a checker for a pure type system to the full CIC.We then turn our attention to the elaborator with the objective to obtain a simple implementation thanks to the features of the programming language. In particular, we want to use λProlog’s unification variables to model the object language ones. In this way, scope checking, carrying of assignments and occur checking are handled by the programming language.We observe that the eager generative semantics inherited from Prolog clashes with this plan. We propose an extension to λProlog that allows to control the generative semantics, suspend goals over flexible terms turning them into constraints, and finally manipulate these constraints at the meta-meta level via constraint handling rules.We implement the proposed language extension in the Embedded Lambda Prolog Interpreter system and we discuss how it can be used to extend the kernel into an elaborator for CIC.

A REUSE-ORIENTED WORKFLOW DEFINITION LANGUAGE

2003 ◽  
Vol 12 (01) ◽  
pp. 1-36 ◽  
Author(s):  
MARIE JOSÉ BLIN ◽  
JACQUES WAINER ◽  
CLAUDIA BAUZER MEDEIROS
Keyword(s):  
Programming Languages ◽  
Building Blocks ◽  
Database Systems ◽  
Exception Handling ◽  
Control Flow ◽  
New Formalism ◽  
Definition Of ◽  
High Level ◽  
And Control ◽  
High Degree

This paper presents a new formalism for workflow process definition, which combines research in programming languages and in database systems. This formalism is based on creating a library of workflow building blocks, which can be progressively combined and nested to construct complex workflows. Workflows are specified declaratively, using a simple high level language, which allows the dynamic definition of exception handling and events, as well as dynamically overriding workflow definition. This ensures a high degree of flexibility in data and control flow specification, as well as in reuse of workflow specifications to construct other workflows. The resulting workflow execution environment is well suited to supporting cooperative work.

Knowledge-based systems, Lisp, and very high level implementation languages

1992 ◽  
Vol 7 (2) ◽  
pp. 147-155
Author(s):  
Eric Sandewall
Keyword(s):  
Operating System ◽  
Programming Languages ◽  
Knowledge Based Systems ◽  
Machine Code ◽  
Low Level ◽  
Knowledge Based ◽  
High Level ◽  
Very High

AbstractIt is usually agreed that programming languages for implementing (other) programming languages, or ‘implementation languages’, should be simple low-level languages which are close to the machine code and to the operating system. In this paper it is argued that a very high level implementation language is a good idea, of particular importance for knowledge-based systems, and that Lisp (as a language and as a system) is very well suited to be a very high level implementation language. The significance of special-purpose programming languages is also discussed, and the requirements that they have for a very high level implementation language are considered.

scholarly journals Bottom-Up Parser: Look-Ahead LR Parser

2019 ◽  
Vol 8 (3) ◽  
pp. 2406-2410
Keyword(s):  
Second Step ◽  
Minimization Algorithm ◽  
Machine Code ◽  
Top Down ◽  
State Problem ◽  
Bottom Up ◽  
Look Ahead ◽  
High Level ◽  
The Given ◽  
Lexical Analyzer

Compiler is used for the purpose of converting high level code to machine code. For doing this procedure we have six steps. On these steps the syntax analyses is the second step of compiler. The lexical analyzer produce token in the output. The tokens are used as input to syntax analyzer. Syntax analyzer performs parsing operation. The parsing can be used for deriving the string from the given grammar called as derivation. It depend upon how derivation will be performed either top down or bottom up. The bottom up parsers LR (Left-to-right), SLR (simple LR) has some conflicts. To remove these conflicts we use LALR (Look ahead LR parser). The conflicts are available if the state contains minimum two or more productions. If there is one shift operation in state and other one is reduce operation it means that shift-reduce operation at the same time. Then this state is called as inadequate state. This Inadequate state problem is solved in LALR parser. Other problem with other parsers is that they have more states as compared to LALR parser. So cost will be high. But in LALR parser minimum states used and cost will automatically be reduced. LALR is also called as Minimization algorithm of CLR (Canonical LR parser).

Modification of Head Droop during Conversation in a 3-Year-Old Visually Impaired Child: A Case Study

1984 ◽  
Vol 78 (7) ◽  
pp. 307-310 ◽  
Author(s):  
Sharon Raver
Keyword(s):  
Early Intervention ◽  
Visually Impaired ◽  
Head Orientation ◽  
Social Reinforcement ◽  
Impaired Child ◽  
Teaching Procedure ◽  
Game Format ◽  
High Level ◽  
High Degree

This study demonstrates a systematic teaching procedure for eliminating head droop in a 3-year-old congenitally visually impaired child. Training consisted of physical prompting and the use of physical and social reinforcement within a game format designed to increase proper head orientation. Results indicated successful amelioration of head droop in training and a high degree of generalization to untrained settings. A high level of maintenance was recorded two weeks following completion of the study. Implications of early intervention in all aspects of social training for the visually impaired are discussed.

MetaJC++: A flexible and automatic program transformation technique using meta framework

2014 ◽  
Vol 4 (3) ◽  
Author(s):  
Nadera Beevi ◽  
M. Reghu ◽  
D. Chitraprasad ◽  
S. Vinodchandra
Keyword(s):  
Programming Languages ◽  
Program Transformation ◽  
Object Oriented Programming ◽  
Intermediate Representation ◽  
Machine Code ◽  
Abstract Syntax Tree ◽  
Source Program ◽  
High Level ◽  
Writing Tools ◽  
New Machine

AbstractCompiler is a tool to translate abstract code containing natural language terms to machine code. Meta compilers are available to compile more than one languages. We have developed a meta framework intends to combine two dissimilar programming languages, namely C++ and Java to provide a flexible object oriented programming platform for the user. Suitable constructs from both the languages have been combined, thereby forming a new and stronger Meta-Language. The framework is developed using the compiler writing tools, Flex and Yacc to design the front end of the compiler. The lexer and parser have been developed to accommodate the complete keyword set and syntax set of both the languages. Two intermediate representations have been used in between the translation of the source program to machine code. Abstract Syntax Tree has been used as a high level intermediate representation that preserves the hierarchical properties of the source program. A new machine-independent stack-based byte-code has also been devised to act as a low level intermediate representation. The byte-code is essentially organised into an output class file that can be used to produce an interpreted output. The results especially in the spheres of providing C++ concepts in Java have given an insight regarding the potential strong features of the resultant meta-language.

scholarly journals A case study in programming coinductive proofs: Howe’s method

2018 ◽  
Vol 29 (8) ◽  
pp. 1309-1343 ◽  
Author(s):  
ALBERTO MOMIGLIANO ◽  
BRIGITTE PIENTKA ◽  
DAVID THIBODEAU
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Abstract Syntax ◽  
Closure Operation ◽  
Formal Reasoning ◽  
Reasoning System ◽  
Contextual Equivalence ◽  
High Level

Bisimulation proofs play a central role in programming languages in establishing rich properties such as contextual equivalence. They are also challenging to mechanize, since they require a combination of inductive and coinductive reasoning on open terms. In this paper, we describe mechanizing the property that similarity in the call-by-name lambda calculus is a pre-congruence using Howe’s method in the Beluga formal reasoning system. The development relies on three key ingredients: (1) we give a higher order abstract syntax (HOAS) encoding of lambda terms together with their operational semantics as intrinsically typed terms, thereby avoiding not only the need to deal with binders, renaming and substitutions, but keeping all typing invariants implicit; (2) we take advantage of Beluga’s support for representing open terms using built-in contexts and simultaneous substitutions: this allows us to directly state central definitions such as open simulation without resorting to the usual inductive closure operation and to encode very elegantly notoriously painful proofs such as the substitutivity of the Howe relation; (3) we exploit the possibility of reasoning by coinduction in Beluga’s reasoning logic. The end result is succinct and elegant, thanks to the high-level abstractions and primitives Beluga provides. We believe that this mechanization is a significant example that illustrates Beluga’s strength at mechanizing challenging (co)inductive proofs using HOAS encodings.

Work Life Balance Of Female Crew In The Aviation Industry: A Case Study

GIS Business ◽  
2019 ◽  
Vol 14 (6) ◽  
pp. 206-212
Author(s):  
Dr. D. Shoba ◽  
Dr. G. Suganthi
Keyword(s):  
Family Life ◽  
Work Life ◽  
Work Life Balance ◽  
Aviation Industry ◽  
Life Balance ◽  
International Airport ◽  
Work Pressure ◽  
Women Employees ◽  
High Level

Employees and employers are facing issues in work life balance. It has become a difficult domain now, because the work needs have increased due to an increase in work pressure and complexities in handling the technology. As there are drastic changes in the rules and regulations in the work scenario of the aviation industry, it makes work life balance of employees difficult and set more hurdles. Hence there are many distractions and imbalances in the life of women employees in the aviation industry working across all levels. This work pressure is creating high level of hurdles in maintaining a harmonious job and family life, especially for female aviation employees. Data is collected from 50 female crew members working at Cochin International Airport. The objective of this study is to analyze the work life balance of working females of Cochin International Airport and its influence on their personal and specialized lives. The result of the study shows that the management should frame certain policies which will help employees to have the balance among their personal and expert lives.

Sign in / Sign up

Export Citation Format

Share Document