A framework for reasoning about inherent parallelism in modern object-oriented languages

With the emergence of multi-core processors into the mainstream, parallel programming is no longer the specialized domain it once was. There is a growing need for systems to allow programmers to more easily reason about data dependencies and inherent parallelism in general purpose programs. Many of these programs are written in popular imperative programming languages like Java and C]. In this thesis I present a system for reasoning about side-effects of evaluation in an abstract and composable manner that is suitable for use by both programmers and automated tools such as compilers. The goal of developing such a system is to both facilitate the automatic exploitation of the inherent parallelism present in imperative programs and to allow programmers to reason about dependencies which may be limiting the parallelism available for exploitation in their applications. Previous work on languages and type systems for parallel computing has tended to focus on providing the programmer with tools to facilitate the manual parallelization of programs; programmers must decide when and where it is safe to employ parallelism without the assistance of the compiler or other automated tools. None of the existing systems combine abstraction and composition with parallelization and correctness checking to produce a framework which helps both programmers and automated tools to reason about inherent parallelism. In this work I present a system for abstractly reasoning about side-effects and data dependencies in modern, imperative, object-oriented languages using a type and effect system based on ideas from Ownership Types. I have developed sufficient conditions for the safe, automated detection and exploitation of a number task, data and loop parallelism patterns in terms of ownership relationships. To validate my work, I have applied my ideas to the C] version 3.0 language to produce a language extension called Zal. I have implemented a compiler for the Zal language as an extension of the GPC] research compiler as a proof of concept of my system. I have used it to parallelize a number of real-world applications to demonstrate the feasibility of my proposed approach. In addition to this empirical validation, I present an argument for the correctness of the type system and language semantics I have proposed as well as sketches of proofs for the correctness of the sufficient conditions for parallelization proposed.

Enhancing Kerr nonlinearity via spontaneously generated coherence

A theoretical investigation is carried out into the effect of spontaneously generated coherence on the Kerr nonlinearity of general three-level systems of Lambda, ladder, and V-shape types. It is found, with spontaneously generated coherence present, that the Kerr nonlinearity can be clearly enhanced. In the Lambda- and ladder-type systems, the maximal Kerr nonlinearity increases and at the same time enters the electromagnetically induced transparency window as the spontaneously generated coherence intensifies. As for the V-type system, the absorption property is significantly modified and therefore enhanced Kerr nonlinearity without absorption occurs for certain probe detunings. We attribute the enhancement of Kerr nonlinearity mainly to the presence of an extra atomic coherence induced by the spontaneously generated coherence.

Creation of arbitrary coherent superposition states in four-level systems

Using the technique of stimulated Raman adiabatic passage, we propose schemes for creating arbi- trary coherent superposition states of atoms in four-level systems: a A-type system with twofold final states and a four-level ladder system. With the use of a control field, arbitrary coherent superposition states are created without the condition of multiphoton resonance. Suitable manipulation of detunings and the control field can create either a single state or any superposition states desired. (c) 2005 Pleiades Publishing, Inc.

The effect of the incident relative phase on the four-wave mixing field and the electromagnetically induced transparency

In a A-type system employing a two-photon pump field, a four-wave mixing field can be generated simultaneously and, hence, a closed-loop system forms. We study theoretically the effect of the relative phase between the two incident fields on the generated four-wave mixing field and the electromagnetically induced transparency. It is found that the phase of the generated four-wave mixing field is the sum of the incident relative phase and a fixed phase that is irrelative to the incident relative phase. Hence, the total phase of the closed-loop system is independent of the incident relative phase. As a result, the incident relative phase has no effect on the electromagnetically induced transparency, which is different from the case of a A-type loop system closed by a third incident field. (c) 2005 Pleiades Publishing, Inc.

开放V型系统中自发辐射诱导相干的影响

利用开放的V型三能级原子系统密度矩阵运动方程的数值解，从不同角度研究了原子自发辐射诱导相干(SGC)对系统吸收和色散的影响。研究发现，这种相干性可导致无粒子数反转激光(LWI)、电磁感应透明(EIT)和无吸收高色散。研究还表明，这种相干性越强，获得最大无反转增益所需的驱动场Rabi频率的值越大而所需的非相干泵浦速率R的值越小；随着原子退出速率的增大，无反转增益逐渐减小并最终转变为吸收，而且增益减小的速度随这种相干性的增强而加快。

Enhancement of Kerr nonlinearity with vanishing absorption in a tripod scheme

The giant enhancement of Kerr nonlinearity in a four-level tripod type system is investigated theoretically. By tuning the value of the Rabi frequency of the coherent control field, owing to the double dark resonances, the giant-enhanced Kerr nonlinearity can be achieved within the right transparency window. The in fluence of Doppler broadening is also discussed.

Fetntosecond pulse shaping with space-to-time conversion based on planar optics

We propose a novel structure of planar optical configuration for implementation of the space-to-time conversion for femtosecond pulse shaping. The previous apparatuses of femtosecond pulse shaping are 4f Fourier-transforming type system that is usually large, expensive, difficult to align. The planar integration of free-space optical systems on solid substrates is an optical module with the attractive advantages of compact, reliable and robust. This apparatus is analyzed in details and the design of the particular lens for femtosecond pulse shaping based on planar optics is presented. (c) 2006 Elsevier GmbH. All rights reserved.

分布计算环境中实现对象互操作的联邦交易模型

本文依据分布计算环境（ＤＣＥ）中所提供的目录服务并结合开放分布处理（ＯＤＰ）所提供的交易服务（ＴｒａｄｉｎｇＳｅｒｖｉｃｅｓ），提出了实现分布计算环境中对象互操作的联邦交易模型。给出了该交易模型在ＤＣＥ中的实现结构模型。

Programming Examples Needing Polymorphic Recursion

Inferring types for polymorphic recursive function definitions (abbreviated to polymorphic recursion) is a recurring topic on the mailing lists of popular typed programming languages. This is despite the fact that type inference for polymorphic recursion using for all-types has been proved undecidable. This report presents several programming examples involving polymorphic recursion and determines their typability under various type systems, including the Hindley-Milner system, an intersection-type system, and extensions of these two. The goal of this report is to show that many of these examples are typable using a system of intersection types as an alternative form of polymorphism. By accomplishing this, we hope to lay the foundation for future research into a decidable intersection-type inference algorithm. We do not provide a comprehensive survey of type systems appropriate for polymorphic recursion, with or without type annotations inserted in the source language. Rather, we focus on examples for which types may be inferred without type annotations.

StaXML: Static Typing of XML Document Fragments for Imperative Web Scripting Languages

We present a type system, StaXML, which employs the stacked type syntax to represent essential aspects of the potential roles of XML fragments to the structure of complete XML documents. The simplest application of this system is to enforce well-formedness upon the construction of XML documents without requiring the use of templates or balanced "gap plugging" operators; this allows it to be applied to programs written according to common imperative web scripting idioms, particularly the echoing of unbalanced XML fragments to an output buffer. The system can be extended to verify particular XML applications such as XHTML and identifying individual XML tags constructed from their lexical components. We also present StaXML for PHP, a prototype precompiler for the PHP4 scripting language which infers StaXML types for expressions without assistance from the programmer.

Examples of Network Flow Verification Using TRAFFIC(X)

In our previous work, we developed TRAFFIC(X), a specification language for modeling bi-directional network flows featuring a type system with constrained polymorphism. In this paper, we present two ways to customize the constraint system: (1) when using linear inequality constraints for the constraint system, TRAFFIC(X) can describe flows with numeric properties such as MTU (maximum transmission unit), RTT (round trip time), traversal order, and bandwidth allocation over parallel paths; (2) when using Boolean predicate constraints for the constraint system, TRAFFIC(X) can describe routing policies of an IP network. These examples illustrate how to use the customized type system.

Faithful Translations between Polyvariant Flows and Polymorphic Types

Recent work has shown equivalences between various type systems and flow logics. Ideally, the translations upon which such equivalences are based should be faithful in the sense that information is not lost in round-trip translations from flows to types and back or from types to flows and back. Building on the work of Nielson & Nielson and of Palsberg & Pavlopoulou, we present the first faithful translations between a class of finitary polyvariant flow analyses and a type system supporting polymorphism in the form of intersection and union types. Additionally, our flow/type correspondence solves several open problems posed by Palsberg & Pavlopoulou: (1) it expresses call-string based polyvariance (such as k-CFA) as well as argument based polyvariance; (2) it enjoys a subject reduction property for flows as well as for types; and (3) it supports a flow-oriented perspective rather than a type-oriented one.

What Are Polymorphically-Typed Ambients?

Abstract: The Ambient Calculus was developed by Cardelli and Gordon as a formal framework to study issues of mobility and migrant code. We consider an Ambient Calculus where ambients transport and exchange programs rather that just inert data. We propose different senses in which such a calculus can be said to be polymorphically typed, and design accordingly a polymorphic type system for it. Our type system assigns types to embedded programs and what we call behaviors to processes; a denotational semantics of behaviors is then proposed, here called trace semantics, underlying much of the remaining analysis. We state and prove a Subject Reduction property for our polymorphically typed calculus. Based on techniques borrowed from finite automata theory, type-checking of fully type-annotated processes is shown to be decidable; the time complexity of our decision procedure is exponential (this is a worst-case in theory, arguably not encountered in practice). Our polymorphically-typed calculus is a conservative extension of the typed Ambient Calculus originally proposed by Cardelli and Gordon.

Typed Abstraction of Complex Network Compositions

The heterogeneity and open nature of network systems make analysis of compositions of components quite challenging, making the design and implementation of robust network services largely inaccessible to the average programmer. We propose the development of a novel type system and practical type spaces which reflect simplified representations of the results and conclusions which can be derived from complex compositional theories in more accessible ways, essentially allowing the system architect or programmer to be exposed only to the inputs and output of compositional analysis without having to be familiar with the ins and outs of its internals. Toward this end we present the TRAFFIC (Typed Representation and Analysis of Flows For Interoperability Checks) framework, a simple flow-composition and typing language with corresponding type system. We then discuss and demonstrate the expressive power of a type space for TRAFFIC derived from the network calculus, allowing us to reason about and infer such properties as data arrival, transit, and loss rates in large composite network applications.

A Formal Semantics for Weak References

A weak reference is a reference to an object that is not followed by the pointer tracer when garbage collection is called. That is, a weak reference cannot prevent the object it references from being garbage collected. Weak references remain a troublesome programming feature largely because there is not an accepted, precise semantics that describes their behavior (in fact, we are not aware of any formalization of their semantics). The trouble is that weak references allow reachable objects to be garbage collected, therefore allowing garbage collection to influence the result of a program. Despite this difficulty, weak references continue to be used in practice for reasons related to efficient storage management, and are included in many popular programming languages (Standard ML, Haskell, OCaml, and Java). We give a formal semantics for a calculus called λweak that includes weak references and is derived from Morrisett, Felleisen, and Harper’s λgc. λgc formalizes the notion of garbage collection by means of a rewrite rule. Such a formalization is required to precisely characterize the semantics of weak references. However, the inclusion of a garbage-collection rewrite-rule in a language with weak references introduces non-deterministic evaluation, even if the parameter-passing mechanism is deterministic (call-by-value in our case). This raises the question of confluence for our rewrite system. We discuss natural restrictions under which our rewrite system is confluent, thus guaranteeing uniqueness of program result. We define conditions that allow other garbage collection algorithms to co-exist with our semantics of weak references. We also introduce a polymorphic type system to prove the absence of erroneous program behavior (i.e., the absence of “stuck evaluation”) and a corresponding type inference algorithm. We prove the type system sound and the inference algorithm sound and complete.