Concurrent Constraint Programming:A Language and Its Execution Model

To overcome inefficiency in traditional logic programming, a declarative programming language COPS is designed based on the notion of concurrent constraint programming (CCP). The improvement is achieved by the adoption of constraint-based heuristic strategy and the introduction of deterministic components in the framework of CCP. Syntax specification and an operational semantic description are presented.

A Comparative Study on Test Case Generation of Concurrent Programs

This paper deals with a comparative study on testing of concurrent programs based on different techniques. The various challenges in testing concurrent programming are: defining test coverage criteria based on control flow, generating control flow graph of nondeterministic programs, investigating the applicability of sequential testing criteria to parallel program testing etc. For solving these issues, some existing techniques are discussed in this study. Various researchers use an intermediate graph called Event Inter Actions Graph (EIAG) to solve the problem of generating the control flow graph of nondeterministic programs. Some researches propose an intermediate graph called Interaction Sequence Testing Criteria (ISTC) approach based on sequence of interactions to solve the problem of test coverage criteria based on control and data flow. Another method to solve the problem of generating test coverage based on control flow graph of nondeterministic programs is constraint based approach. It needs constrained elements to generate test case which includes structural element and constraint. The selection of good test cases has been addressed by test data generation technique. The technique of concurrent path analysis approach is used to solve the problem of applicability of sequential testing criteria to parallel program testing. It reduces the number of combined concurrent test paths. The sequential test paths are combined to form concurrent test path. The Integration and System Test Automation (ISTA) approach is used to solve the problem of applicability of sequential testing criteria to parallel program testing. It is used for automated test case generation and execution by using high-level Petri net is a finite state test model.

Strategic mining options optimization:Open pit mining, underground mining or both

Near-surface deposits that extend to considerable depths are often amenable to both open pit mining and/or underground mining. This paper investigates the strategy of mining options for an orebody using a Mixed Integer Linear Programming(MILP) optimization framework. The MILP formulation maximizes the Net Present Value(NPV) of the reserve when extracted with(i) open pit mining,(ii) underground mining, and(iii) concurrent open pit and underground mining. Comparatively, implementing open pit mining generates a higher NPV than underground mining. However considering the investment required for these mining options, underground mining generates a better return on investment than open pit mining. Also, in the concurrent open pit and underground mining scenario, the optimizer prefers extracting blocks using open pit mining. Although the underground mine could access ore sooner, the mining cost differential for open pit mining is more than compensated for by the discounting benefits associated with earlier underground mining.

Precise slicing of interprocedural concurrent programs

Program slicing is an effective technique for an- alyzing concurrent programs. However, when a conventional closure-based slicing algorithm for sequential programs is ap- plied to a concurrent interprocedural program, the slice is usually imprecise owing to the intransitivity of interference dependence. Interference dependence arises when a state- ment uses a variable defined in another statement executed concurrently. In this study, we propose a global dependence analysis approach based on a program reachability graph, and construct a novel dependence graph called marking-statement dependence graph （MSDG）, in which each vertex is a 2-tuple of program state and statement. In contrast to the conven- tional program dependence graph where the vertex is a state- ment, the dependence relation in MSDG is transitive. When traversing MSDG, a precise slice will be obtained. To en- hance the slicing efficiency without loss of precision, our slic- ing algorithm adopts a hybrid strategy. The procedures con- taining interaction statements between threads are inlined and sliced by the slicing algorithm based on program reachability graphs while allowing other procedures to be sliced as se- quential programs. We have implemented our algorithm and three other representative slicing algorithms, and conducted an empirical study on concurrent Java programs. The exper- imental results show that our algorithm computes more pre- cise slices than the other algorithms. Using partial-order re- duction techniques, which are effective for reducing the size of a program reachability graph without loss of precision, ouralgorithm is optimized, thereby improving its performance to some extent.

Verification of Concurrent Assembly Programs with a Petri Net Based Safety Policy

Concurrent programs written in a machine level language are being used in many areas but verification of such programs brings new challenges to the programming language community. Most of the studies in the literature on verifying the safety properties of concurrent programs are for high-level languages, specifications, or calculi. Therefore, more studies are needed on concurrency verification for machine level language programs. This paper describes a framework of a Petri net based safety policy for the verification of concurrent assembly programs, to exploit the capability of Petri nets in concurrency modeling. The concurrency safety properties can be considered separately using the net structure and by mixing Hoare logic and computational tree logic. Therefore, more useful higher-level safety properties can be specified and verified.

Certifying Concurrent Programs Using Transactional Memory

Transactional memory （TM） is a new promising concurrency-control mechanism that can avoid many of the pitfalls of the traditional lock-based techniques. TM systems handle data races between threads automatically so that programmers do not have to reason about the interaction of threads manually. TM provides a programming model that may make the development of multi-threaded programs easier. Much work has been done to explore the various implementation strategies of TM systems and to achieve better performance, but little has been done on how to formally reason about programs using TM and how to make sure that such reasoning is sound. In this paper, we focus on the semantics of transactional memory and present a proof-carrying code （PCC） system for reasoning about programs using TM . We formalize our reasoning with respect to the TM semantics, prove its soundness, and use examples to demonstrate its effectiveness.

SYN-Sequence Selection Strategy for Testing Concurrent Programs Based on Little Strong Happened-Before

This paper defines a new relation--little strong happened-before（LSHB） and presents the algorithm for LSHB. Compared with strong happened-before （SHB） and weak happened- before （WHB）, LSHB supports keeping-read-result and ensures definite sufficiency of testing. Equivalence partitioning the set of SYN-sequences based on LSHB can efficiently reduce the number of testing SYN-sequences. The case studies prove that LSHB has high practicability.

ρ Graph: Rendezvous Ordering Graph forAda Concurrent Programs

In disciplined Ada software development and maintenance, an adequate and suitable graphical representation for concurrency is important. To describe rendezvous ordering, tasking andexecuting flow of tasks, p graph--Rendezvous Ordering Graph is presenced in this paper. pgraph is a kind of-hierarchical oriented graph with nodes representing rendezvouses and edgesshowing'ordering relations between rendezvouses as well as flow of tasks. It can be used insoftware understanding, design description and documentation.