Kiko Fernandez-Reyes

Dave Clarke

Daniel S Mccain

ParT: An Asynchronous Parallel Abstraction for Speculative Pipeline Computations

The ubiquity of multicore computers has forced programming language designers to rethink how languages express parallelism and concurrency. This has resulted in new language constructs and new combinations or revisions of existing constructs. In this line, we extended the programming languages Encore (actor-based), and Clojure (functional) with an asynchronous parallel abstraction called ParT, a data structure that can dually be seen as a collection of asynchronous values (integrating with futures) or a handle to a parallel computation, plus a collection of combinators for manipulating the data structure. The combinators can express parallel pipelines and speculative parallelism. This paper presents a typed calculus capturing the essence of ParT, abstracting away from details of the Encore and Clojure programming languages. The calculus includes tasks, futures, and combinators similar to those of Orc but implemented in a non-blocking fashion. Furthermore, the calculus strongly mimics how ParT is implemented, and it can serve as the basis for adaptation of ParT into different languages and for further extensions.

Introduction

The ubiquity of multicore computers has forced programming language designers to rethink how languages express parallelism and concurrency. This has resulted in new language constructs that, for instance, increase the degree of asynchrony while exploiting parallelism. A promising direction is programming languages with constructs for tasks and actors, such as Clojure and Scala [START_REF] Hickey | The Clojure programming language[END_REF][START_REF] Odersky | Programming in Scala: A Comprehensive Step-by-step Guide[END_REF], due to the lightweight overhead of spawning parallel computations. These languages offer coarse-grained parallelism at the task and actor level, where futures act as synchronisation points. However, these languages are lacking in high-level coordination constructs over these asynchronous computations. For instance, it is not easy to express dependence on the first result returned via a bunch of futures and to safely terminate the computations associated with the other futures. The task of terminating speculative parallelism is quite delicate, as the futures may have attached parallel computations that depend on other futures, creating complex dependency patterns that need to be tracked down and terminated.

To address this need, this paper presents the design and implementation of ParT, a non-blocking abstraction that asynchronously exploits futures and enables the developer to build complex, data parallel coordination workflows using high-level constructs. These high-level constructs are derived from the combinators of the orchestration language Orc [START_REF] Kitchin | A language for task orchestration and its semantic properties[END_REF][START_REF] Kitchin | The Orc programming language[END_REF]. ParT is formally expressed in terms of a calculus that, rather than being at a high level of abstraction, strongly mimics how this asynchronous abstraction is implemented and is general enough to be applied to programming languages with notions of futures.

The contributions of the paper are as follows: the design of an asynchronous parallel data abstraction to coordinate complex workflows, including pipeline and speculative parallelism, and a typed, non-blocking calculus modelling this abstraction, which integrates futures, tasks and Orc-like combinators, supports the separation of the realisation of parallelism (via tasks) from its specification, and offers a novel approach to terminating speculative parallelism.

Overview

To set the scene for this paper, we begin with a brief overview to asynchronous computations with futures and provide an informal description of the ParT abstraction and its combinators. A SAT solver example is used as an illustration.

In languages with notions of tasks and active objects [START_REF] Brandauer | Parallel objects for multicores: A glimpse at the parallel language Encore[END_REF][START_REF] Hickey | The Clojure programming language[END_REF][START_REF] Odersky | Programming in Scala: A Comprehensive Step-by-step Guide[END_REF], asynchronous computations are created by spawning tasks or calling methods on active objects. These computations can exploit parallelism by decoupling the execution of the caller and the callee [START_REF] Robert | Multilisp: A language for concurrent symbolic computation[END_REF]. The result of a spawn or method call is immediately a future, a container that will eventually hold the result of the asynchronous computation. A future that has received a value is said to be fulfilled. Operations on futures may be blocking, such as getting the result from a future, or may be asynchronous, such as attaching a callback to a future. This second operation, called future chaining and represented by f callback , immediately returns a new future, which will contain the result of applying the callback function callback to the contents of the original future after it has been fulfilled. A future can also be thought of as a handle to an asynchronous computation that can be extended via future chaining or even terminated. This is an useful perspective that we will further develop in this work. In languages with notions of actors, such as Clojure and Encore [START_REF] Brandauer | Parallel objects for multicores: A glimpse at the parallel language Encore[END_REF], asynchrony is the rule and blocking on futures suffers a large performance penalty. But creating complex coordination patterns based on a collection of asynchronous computations without blocking threads (to maintain the throughput of the system) is no easy task.

To address this need, we have designed an abstraction, called ParT, which can be thought of as a handle to an ongoing parallel computation, allowing the parallel computation to be manipulated, extended, and terminated. A ParT is a functional data structure, represented by type Par t, that can be empty {} :: Par t, contain a single expression {-} :: t → Par t, or futures attached to computations producing values, using (-) • :: Fut t → Par t, or computations producing ParTs, embedded using (-) † :: Fut (Par t) → Par t. Multiple ParTs Fig. 1: A SAT solver in Encore. can be combined using the par constructor, :: Par t → Par t → Par t. This constructor does not necessarily create new parallel threads of control, as this would likely have a negative impact on performance, but rather specifies that parallelism is available. The scheduler in the ParT implementation can choose to spawn new tasks as it sees fit -this is modelled in the calculus as a single rule that nondeterministically spawns a task from a par (rule Red-Schedule).

The combinators can express complex coordination patterns and operate on them in a non-blocking manner, and safely terminate speculative parallelism even in the presence of complex workflows. These combinators will be illustrated using an example, then explained in more detail.

Illustrative example. Consider a portfolio-based SAT solver (Fig. 1), which creates numerous strategies, of which each finds an assignment of variables to Boolean values for a given proposition, runs them in parallel, and accepts the first solution found. Each strategy tries to find a solution by selecting a variable and creating two instances of the formula, one where the variable is assigned true, the other where it is assigned false (called splitting) -strategies differ in the order they select variables for splitting. These new instances can potentially be solved in parallel.

The example starts in function process (line 20) which receives an array of strategies and the formula to solve. Strategies do not interact with each other and can be lifted to a ParT, creating a parallel pipeline (line 21) using the each and bind ( =) combinators. As soon as one strategy finds an assignment, the remaining computations are terminated via the prune ( ) combinator.

For each strategy, a call to the sat function (line 8) is made in parallel using a call to async, which in this case returns a value of type Fut (Par Assignment). Function sat takes three arguments: a strategy, a formula and an assignment object containing the current mapping from variables to values. This function uses the strategy object to determine which variable to split next, extends the assignment with new valuations (lines 9-11), recursively solves the formula (by again calling sat), and returns an assignment object if successful. The evaluation of the formula, evaluateFormula returns, firstly, an optional Boolean to indicate whether evaluation has completed, and if it has completed, whether the formula is satisfiable, and secondly, the current (partial) variable assignment. The two calls to evaluateFormula are grouped into a new ParT collection (using || ) and, with the use of the = combinator, a new asynchronous pipeline is created to either further evaluate the formula by calling sat, to return the assignment in the case that a formula is satisfiable as a singleton ParT, or {} when the assignment does not satisfy the formula (lines [START_REF] Martí | Rewriting logic: roadmap and bibliography[END_REF][START_REF] Mccain | Parallel combinators for the Encore programming language[END_REF][START_REF] Odersky | Programming in Scala: A Comprehensive Step-by-step Guide[END_REF][START_REF] Peierls | Java Concurrency in Practice[END_REF][START_REF] Prokopec | A generic parallel collection framework[END_REF].

Finally, returning back to process, the prune combinator ( ) (line 21) is used to select the first result returned by the recursive calls to sat, if there is one. This result is converted from an option type to an empty or singleton ParT collection (again asynchronously), which can then be used in a larger parallel operation, if so desired. The prune combinator will begin poisoning and safely terminating the no longer needed parallel computations, which in this case will be an ongoing parallel pipeline of calls to sat and evaluateFormula.

ParT Combinators. The combinators are now described in detail. The combinators manipulate ParT collections and were derived from Orc [START_REF] Kitchin | A language for task orchestration and its semantic properties[END_REF][START_REF] Kitchin | The Orc programming language[END_REF], although in our setting, they are typed and redefined to be completely asynchronous, never blocking the thread. Primitive combinators express coordination patterns such as pipeline and speculative parallelism, and more complex patterns can be expressed based on these primitives.

Pipeline parallelism is expressed in ParT with the sequence and bind combinators. The sequence combinator, :: Par t → (t → t ) → Par t , takes a ParT collection and applies the function to each element in the collection, potentially in parallel, returning a new ParT collection. The bind combinator (derived from other combinators) = :: Par t → (t → Par t ) → Par t is similar to the sequence combinator, except that the function returns a ParT collection and the resulting nested ParT collection is flattened. (Par is a monad!1 ) In the presence of futures inside a ParT collection, these combinators use the future chaining operation to create independent and asynchronous pipelines of work.

Speculative parallelism is realised by the peek combinator, peek :: Par t → Fut (Maybe t), which sets up a speculative computation, asynchronously waits for a single result to be produced, and then safely terminates the speculative work. To terminate speculative work the ParT abstraction poison these specu-lative computations, which may have long parallel pipelines to which the poison spreads recursively, producing a pandemic infection among futures, tasks and pipelines of computations. Afterwards, poisoned computations that are no longer needed can safely be terminated. Metaphorically, this is analogous to a tracing garbage collector.

The value produced by peek is a future to an option type. The option type is used to capture whether the parallel collection was empty or not. The empty collection {} results in Nothing, and a non-empty collection results in a Just v, where v is the first value produced. The conversion to option type is required because ParTs cannot be tested for emptiness without blocking. The peek combinator is an internal combinator, i.e., it is not available to the developer and is used by the prune combinator (explained below). Built on top of peek is the prune combinator, :: (Fut (Maybe t) → Par t ) → Par t → Par t , which applies a function in parallel to the future produced by peek, and returns a parallel computation.

Powerful combinators can be derived from the ones mentioned above. An example of a derived combinator, which is a primitive in Orc, is the otherwise combinator, > < :: Par t → Par t → Par t (derivation is shown in Section 3.1). Expression e 1 > < e 2 results in e 1 unless it is an empty ParT, in which case it results in e 2 .

Other ParT combinators are available. For instance, each :: [t] → Par t and extract :: Par t → [t] convert between sequential (arrays) and ParTs. The latter potentially requires a lot of synchronisation, as all the values in the collection need to be realised. Both have been omitted from the formalism, because neither presents any real technical challenge -the key properties of the formalism, namely, deadlock-freedom, type preservation and task safety (Section 3.5), still hold with these extensions in place.

A Typed ParT Calculus

This section presents the operational semantics and type system of a task-based language containing the ParT abstraction. The formal model is roughly based on the Encore formal semantics [START_REF] Brandauer | Parallel objects for multicores: A glimpse at the parallel language Encore[END_REF][START_REF] Clarke | Vats: A safe, reactive storage abstraction[END_REF], with many irrelevant details omitted.

Syntax

The core language (Fig. 2) contains expressions e and values v . Values include constants c, variables, futures f , lambda abstractions, and ParT collections of values. Expressions include values v , function application (e e), task creation, future chaining, and parallel combinators. Tasks are created via the async expression, which returns a future. The parallel combinators are those covered in Section 2 ( || , , peek and ), plus some derived combinators, together with the low-level combinator join that flattens nested ParT collections. Recall that peek is used under-the-hood in the implementation of . Status π controls how peek behaves: when π is and the result in peek is an empty ParT collection, the value is discarded and not written to the corresponding future. This status helps to ensure that precisely one speculative computation writes into the future and that a speculative computation fails to produce a value only when all relevant tasks fail to produce a value. ParT collections are monoids, meaning that the composition operation e || e is associative and has {} as its unit. As such, ParT collections are sequences, though no operations such as getting the first element are available to access them sequentially. As an alternative, adding in commutativity of || would give multiset semantics to the ParT collections -the operational semantics is otherwise unchanged. Two for one! A number of the constructs are defined by translation into other constructs. The encoding of let is standard. In e 1 > < e 2 , pruning is used to test the emptyness of e 1 . If it is not empty, the result of e 1 is returned, otherwise the result is e 2 . The definition of = is a standard definition of monadic bind in terms of map ( ) and join. We assume for convenience a Maybe type and pattern matching on it.

Configurations

Running programs are represented by configurations (Fig. 3). Configurations can refer to the global system or a partial view of the system. A global configuration {config} captures the complete global state, e.g., {(fut f ) (task f e)} shows a global system containing a single task running expression e. Local configurations, written as config, show a partial view of the state of the program. These are multisets of tasks, futures, poison and future chains. The empty configuration is represented by . Future configurations, (fut f ) and (fut f v), represent unfulfilled and fulfilled futures, respectively. Poison is the configuration (poison f ) that will eventually terminate tasks and chains writing to future f and their dependencies. A running task (task α f e) has a body e and will write its result to future f. The chain configuration (chain α f g e) depends on future g that, when fulfilled, will then run expression e on the value stored in g, and write its value into future f. Concatenation of configurations, config config , is associative and commutative with the empty configuration as its unit (Fig. 12).

gconfig ::= {config} config ::= | (fut f ) | (fut f v) | (poison f ) | (task α f e) | (chain α f g e) | config config α ::= |
Tasks and chains have a flag α that indicates the poisoned state of the computation. Whitespace ' ' indicates that the computation has not been poisoned, and indicates that the computation has been poisoned and can be safely terminated, if it is not needed (see Rule Red-Terminate of Fig. 10).

The initial configuration to evaluate expression e is {(task f e) (fut f )}, where the value written into future f is the result of the expression.

Reduction Rules

The operational semantics is based on a small-step, reduction-context based rules for evaluation within tasks, and parallel reduction rules for evaluation across configurations. Evaluation is captured by expression-level evaluation context E containing a hole • that marks where the next step of the reduction will occur (Fig. 4). Plugging an expression e into an evaluation context E, denoted E[e], represents both the subexpression to be evaluated next and the result of reducing that subexpression in context, in the standard fashion [START_REF] Wright | A syntactic approach to type soundness[END_REF].

E ::= • | E e | v E | E e | v E | {E} | E || e | v || E | E e | v E | E e | E • | E † | join E | peek π E
Fig. 4: Expression-level evaluation contexts.

Reduction of configurations is denoted config → config , which states that config reduces in a single step to config .

Core Expressions. The core reduction rules (Fig. 5) for functions, tasks and futures are well-known or derived from earlier work [START_REF] Clarke | Vats: A safe, reactive storage abstraction[END_REF]. Together, the rules Red-Chain and Red-ChainV describe how future chaining works, initially attaching a closure to a future (via the chain configuration), then evaluating the closure in a new task after the future has been fulfilled.

(Red-β-Red) (task α g E[(λx.e) v]) → (task α g E[e[v/x]]) (Red-Async) fresh f (task α g E[async e]) → (fut f ) (task α f e) (task α g E[f ]) (Red-FutV) (task α f v) (fut f ) → (fut f v) (Red-Chain) fresh h (task α g E[f v]) → (fut h ) (chain α h f v) (task α g E[h]) (Red-ChainV) (chain α g f e) (fut f v) → (task α g (e v)) (fut f v)
Fig. 5: Core reduction rules.

Sequencing. The sequencing combinator creates pipeline parallelism. Its semantics are defined inductively on the structure of ParT collections (Fig. 6). The second argument must be a function (tested in function application, but guaranteed by the type system). In Red-SeqS, sequencing an empty ParT results in another empty ParT. A ParT with a value applies the function immediately (Red-SeqV). A lifted future is asynchronously accessed by chaining the function onto it (Red-SeqF). Rule Red-SeqP recursively applies v to the two sub-collections. A future whose content is a ParT collection chains a recursive call to v onto the future and lifts the result back into a ParT collection (Red-SeqFP). Prune and Peek. Pruning is the most complicated part of the calculus, though most of the work is done using the peek combinator (Fig. 8). Firstly, rule Red-

(Red-SeqS) (task α g E[{} v]) → (task α g E[{}]) (Red-SeqV) (task α g E[{v} v ]) → (task α g E[{v v}]) (Red-SeqF) (task α g E[f • v]) → (task α g E[(f v) • ]) (Red-SeqFP) (task α g E[f † v]) → (task α g E[(f (λx.x v)) † ]) (Red-SeqP) (task α g E[(v1 || v2) v]) → (task α g E[(v1 v) || (v2 v)])
(Red-JoinS) (task α g E[join {}]) → (task α g E[{}]) (Red-JoinV) (task α g E[join {v}]) → (task α g E[v]) (Red-JoinF) (task α g E[join f • ]) → (task α g E[f † ]) (Red-JoinFP) (task α g E[join f † ]) → (task α g E[(f (λx.join x)) † ]) (Red-JoinP) (task α g E[join (v1 || v2)]) → (task α g E[(join v1) || (join v2)])
Fig. 7: Reduction rules for the join combinator.

(Red-Prune) fresh f

(task α g E[v v ]) → (fut f ) (task α f (peek v )) (task α g E[v f ]) (Red-PeekS ) (task α g E[peek {}]) → (Red-PeekS) (task α g E[peek {}]) (futg) → (futg Nothing) (poison g) (Red-PeekV) (task α g E[peek π ({v} || v ) ]) (futg) → (futg (Just v)) (poison g) h∈deps(v ) (poison h) (Red-PeekF) (task α g E[peek π (f • || v)]) → (chain α g f (λx.peek π {x})) (task α g (peek v)) (Red-PeekFP) fresh h (task α g E[peek π (f † || v)]) → (chain α g f (λx.peek π (x || (h maybe2par) † ))) (fut h ) (task α h (peek v)) (chain α g h (λx.peek (maybe2par x)))
Fig. 8: Reduction rules for pruning. For singleton collections are handled via equality v = v || {}.

Prune spawns a new task that will peek the collection v , and passes this new task's future to the function v. The essence of the peek rules is to set up a bunch of computations that compete to write into a single future, with the strict requirement that Nothing is written only when all competing tasks cannot produce a value-that is, when the ParT being peeked is empty. This is challenging due to the lifted future ParTs (type Fut (Par t)) within a collection, because such a future may be empty, but this fact cannot easily be seen in a non-blocking way.

Another challenge is to avoid introducing sequential dependencies between entities that can potentially run in parallel, to avoid, for instance, a non-terminating computation blocking one that will produce a result.

A task that produces a ParT containing a value (rule Red-PeekV) writes the value, wrapped in an option type, into the future and poisons all computations writing into that future, recursively poisoning direct dependencies. The status on peek prevents certain peek invocations from writing a final empty result, as in rule Red-PeekS . Contrast with Red-PeekS, in which a task resulting in an empty ParT writes Nothing into the future -in this case it is guaranteed that no other peek exists writing to the future.

A lifted future f is guaranteed to produce a result, though it may not produce it in a timely fashion. This case is handled (rule Red-PeekF) by chaining a function onto it that will ultimately write into future g when the value is produced, if it wins the race. Otherwise, the result of peeking into v is written into g, unless the value produced is {} (which is controlled by ).

A lifted future to a ParT is not necessarily guaranteed to produce a result, and neither is any ParT that runs in parallel with it. Thus, extra care needs to be taken to ensure that Nothing is written if and only if both are actually empty. This is handled in rule Red-PeekFP. Firstly, a function is chained onto the lifted future to get access to the eventual ParT collection. This is combined with future h that is used to peek into v via a new task.

In all cases, computations propagate the poison state α to new configurations.

Scheduling. Rule Red-Schedule (Fig. 9) models the non-deterministic scheduling of parallelism within a task, converting some of the parallelism latent in a ParT collection into a new task. Apart from this rule, expressions within tasks are evaluated sequentially.

(Red-Schedule) fresh f

(task α g E[e1 || e2]) → (task α g E[e1 || f † ]) (fut f ) (task α f e2)
Fig. 9: Spawning of tasks inside a ParT.

Poisoning and Termination. The rules for poisoning and termination (Fig. 10) are based on a poisoned carrier configuration defined as (P C α f e) ::= (task α f e) | (chain α f g e); these rules rely on the definition of when a future is needed (Definition 2), which in turn is defined in terms of the futures on which a task depends to produce a value (Definition 1). Definition 1. The dependencies of an expression e, deps(e), is the set of the futures upon which the computation of e depends in order to produce a value: Definition 2. A future f is needed in configuration config, denoted config needed (f ), whenever some other element of the configuration depends on it: Configurations go through a two step process before being terminated. In the first step (rule Red-Poison) the poisoning of future f poisons any task or chain writing to f , marks it with , and the poison is transmitted to the direct dependencies of the expression e in the task or chain. In the second step (Red-Terminate), a poisoned configuration is terminated when there is no other configuration relying on its result -that is, a poisoned task or chain is terminated if there is no expression around to keep it alive. This rule is global, referring to the entire configuration. Termination can be implemented using tracing garbage collection, though in the semantics a more global specification of dependency is used.

deps(f ) = {f } deps(c) = deps({}) = deps(x ) = ∅
config needed (f ) iff (P C α g e) ∈ config ∧ f ∈ deps((PC α g e)) ∧ (fut f ) ∈ config. (Red-Poison) (poison f ) (P C f e) → (poison f ) (P C f e) g∈deps((PC f e)) (poison g) (Red-Terminate) ¬(config needed(f )) {(P C f e) config} → {config}
An example (Fig. 11) illustrates how poisoning and termination work to prevent a task that is still needed from being terminated. Initially, there is a bunch of tasks (squares) and futures (circles) (Fig. 11A), where one of the tasks completes and writes a value to future f . This causes all of the other tasks writing to f to be poisoned, via Rule Red-PeekV (Fig. 11B). After application of rule Red-Poison, the dependent tasks and futures are recursively poisoned (Fig. 11C). Finally, the application of rule Red-Terminate terminates tasks that are not needed (Fig. 11D). Task e 1 is not terminated, as future g is required by the task computing e g.

Configurations.

The concatenation operation on configurations is commutative and associative and has the empty configuration as its unit (Fig. 12). We assume that these equivalences, along with the monoid axioms for , can be applied at any time during reduction.

The reduction rules for configurations (Fig. 13) have the individual configuration reduction rules at their heart, along with standard rules for parallel evaluation of non-conflicting sub-configurations, as is standard in rewriting logic [START_REF] Martí | Rewriting logic: roadmap and bibliography[END_REF].

Type System

The type system (Fig. 14) assigns the following types to terms:

τ ::= K | Fut τ | Par τ | Maybe τ | τ → τ
where K represents the basic types, Fut τ is the type of a future containing a value of type τ , Par τ is the type of a ParT collection of type τ , Maybe τ represents an option type, and τ → τ represents function types. We also let ρ range over types.

The key judgement in the type system is Γ ρ e : τ which asserts that, in typing context Γ , the expression e is a well-formed term with type τ , where ρ is the expected return type of the task in which this expression appearsρ is required to type peek. The typing context contains the types of both free variables and futures.

Rule TS-Async gives the type for task creation and rule TS-Chain shows how to operate on such values -future chaining has the type of map for the

config → config config config → config config config 0 → config 0 config 1 → config 1 config 0 config 1 → config 0 config 1 config 0 config → config 0 config config 1 config → config 1 config config 0 config 1 config → config 0 config 1 config config → config {config} → {config }
Fig. 13: Configuration reduction rules Fut constructor. Rules TS-EmptyPar, TS-SingletonPar, TS-LiftF, TS-LiftFP, and TS-Par give the typings for constructing ParT collections. Rule TS-Sequence implies that sequencing has the type of map for the Par constructor. TS-Bind and TS-Join give = and join the types of the monadic bind and join operators for the Par constructor, respectively. Rule TS-Prune captures the communication between the two parameters via the future passed as an argument to the first parameter -the future will contain the first value of the second parameter if there is one, captured by the Maybe type. Rule TS-Peek captures the conversion of the singleton or empty argument of peek from Par ρ to Maybe ρ, the expected result type of the surrounding task. Because peek terminates the task and does not return locally, its return type can be any type.

(TS-Const) c is a constant of type τ Γ ρ c : τ (TS-Fut) f : Fut τ ∈ Γ Γ ρ f : Fut τ (TS-X) x : τ ∈ Γ Γ ρ x : τ (TS-App) Γ ρ e1 : τ → τ Γ ρ e2 : τ (TS-Bind) Γ ρ e1 : Par τ Γ ρ e2 : τ → Par τ Γ ρ e1 = e2 : Par τ
Well-formed configurations (Fig. 15) are expressed by the judgement Γ config ok, where Γ is the assumptions about the future types in config. Rules T-Task and T-Chain propagate the eventual expected result type on the turnstyle when typing the enclosed expression. Rule T-Config depends upon the following definition, a function that collects all futures defined in a configuration:

(T-Fut) f ∈ dom(Γ ) Γ (fut f ) ok (T-FutV) f : Fut τ ∈ Γ Γ τ v : τ Γ (fut f v) ok (T-Poison) f : Fut τ ∈ Γ Γ (poison f ) ok (T-Task) f : Fut τ ∈ Γ Γ τ e : τ Γ (task α f e) ok (T-Chain) f1 : Fut τ1 ∈ Γ f2 : Fut τ2 ∈ Γ Γ τ 2 e : τ1 → τ2 Γ (chain α f 2 f1 e) ok (T-Config) Γ config 1 ok Γ config 2 ok futset(config 1 ) ∩ futset(config 2 ) = ∅ Γ config 1 config 2 ok (T-GConfig) Γ config ok dom(Γ ) = futset(config) TaskSafe(config) AcyclicDep(config) Γ {config} ok
Definition 3. Define futset(config) as: futset((fut f )) = futset((fut f v)) = {f } futset((config 1 config 2 )) = futset(config 1 ) ∪ futset(config 2 ) futset( ) = ∅.
Rule T-GConfig defines the well-formedness of global configurations, judgement Γ {config} ok. This rule depends on a number of definitions that capture properties on futures and tasks and on the dependency between futures. The invariance of these properties is ultimately used to proof type soundness and other safety properties of the system. Definition 4. Define the following functions for collecting the different kinds of tasks and chains of a configuration:

regular f (config) = {(task f e) ∈ config | e = peek π e } ∪ {(chain f g e) ∈ config | e = λ . peek π e } peeker f (config) = {(task f (peek e)) ∈ config} ∪ {(chain f g (λ . peek e)) ∈ config} peeker f (config) = {(task f (peek e)) ∈ config} ∪ {((chain f g (λ . peek e)) ∈ config}
Tasks with no peek expression are called regular tasks, while peeker tasks have the peek expression -there are both -and non--peeker tasks. These functions can be used to partition the tasks and chains in a configuration into these three kinds of tasks and chains. These definitions consider peek expressions only at the top level of a task, although the syntax allows them to be anywhere. Based on the reduction rules, one can prove that peek only appears at the top level of a task or chain, so no task or chain is excluded by these definitions. Definition 5. Define predicate TaskSafe(config) as follows:

TaskSafe(config) iff for all f ∈ futset(config) |regular f (config) ∪ peeker f (config)| ≤ 1 ∧ (fut f ) ∈ config ∧ (poison f ) / ∈ config ⇒ |regular f (config) ∪ peeker f (config)| = 1 ∧ |regular f (config)| = 1 ⇒ peeker f (config) ∪ peeker f (config) = ∅ ∧ (task α f (peek {})) ∈ config ⇒ (fut f ) ∈ config ∧ peeker f (config) = ∅
Predicate TaskSafe(config) (Definition 5) describes the structure of the configuration config. It states that:

there is at most one regular or non--peeker task per future; if a future has not yet been fulfilled and it is not poisoned, then there exists exactly one regular task or non--peeker task that fulfils it; regular tasks and peeker tasks do not write to the same futures; and if a peeker task that is about to fulfil a future with Nothing, then the future is unfulfilled and no -peeker task fulfilling the same future exists.

The following definition establishes dependencies between futures. Predicate config f g holds for all future g whose eventual value could influence the result stored in future f . Definition 6. Define the predicate config f g as the least transitive relation satisfying the following rules:

(task α f e) ∈ config g ∈ deps(e) config f g (chain α f h e) ∈ config g ∈ deps(e) ∪ {h} config f g (fut f v) ∈ config g ∈ deps(v ) config f g Definition 7.
Predicate AcyclicDep(config) holds iff relation is acyclic, where is defined for config in Definition 6.

Rule T-GConfig for well-formed global configurations requires that precisely the futures that appear in the typing environment Γ appear in the configuration, that the configuration is well-formed, and that it satisfies the properties TaskSafe and AcyclicDep. By including these properties as a part of the wellformedness rule for global configurations, type preservation (Lemma 1) makes these invariants. These invariants on the structure of tasks and the dependency relation together ensure that well-typed configurations are deadlock-free, as we explore next.

Formal Properties

The calculus is sound and deadlock-free. These results extend previous work [START_REF] Mccain | Parallel combinators for the Encore programming language[END_REF] to address the pruning combinator.

Lemma 1 (Type Preservation). If Γ {config} ok and {config} → {config }, then there exists a Γ such that Γ ⊇ Γ and Γ {config } ok.

Proof. By induction on derivation {config} → {config }. In particular, the invariance of AcyclicDep is shown by considering the changes to the dependencies caused by each reduction rule. The only place where new dependencies are introduced is when new futures are created. Adding a future to the dependency relation cannot introduce cycles.

The following lemma states that the notion of needed, which determines whether or not to garbage collect a poisoned task or chain, is anti-monotonic, meaning that after a future is no longer needed according to the definitions, it does not subsequently become needed.

Lemma 2 (Safe Task Kill). If Γ {config} ok and {config} → {config }, then ¬(config needed (f )) implies ¬(config needed (f )).

Proof. A future is initially created in a configuration where it is needed. If ever a future disappears from deps(e), if can never reappear. This lemma rules out the situation where a task is poisoned and garbage collected, but is subsequently needed. For instance, the application of rule Red-Terminate in Fig. 11C kills tasks e 2 , e 3 , e 5 and e 6 (shown in Fig 11D). If the future into which these tasks were going to write is needed afterwards, there would be a deadlock as a new task could chain on that future but never be fulfilled.

Definition 8 (Terminal Configuration).

A global configuration {config} is terminal iff every element of config has one of the following shapes: (fut f ), (fut f v) or (poison f ).

Lemma 3 (Deadlock-Freedom/Progress). If Γ {config} ok, then config is a terminal configuration, or there exists a config such that {config} → {config }.

Proof. By induction on a derivation of {config} → {config }, relying on the invariance of AcyclicDep and Lemma 2.

Deadlock-freedom guarantees that some reduction rule can be applied to a well-typed, non terminal, global configuration -this is essentially the progress property required to prove type safety. It implies further that there are no local deadlocks, such as a deadlocked configuration like (chain f g e) (chain g f e ). Such a configuration fails to satisfy the AcyclicDep invariant, thus cannot exist. If mutable state is added to the calculus, deadlock-freedom is lost.

Implementations. There are two prototypes of the ParT abstraction. In the first prototype,2 ParT has been written as an extension to the Encore compiler (written in Haskell) and runtime (written in C) but, it can be implemented in well-established languages with notions of tasks and futures. This prototype integrates futures produced by tasks and active objects with the ParT abstraction. The other prototype has been written in Clojure, 3 which is not statically typed. Both prototypes follow the semantics to guide the implementation. In practice, this means that the semantic rules are written in such a way that they can be easily mimicked in a library or in a language runtime.

Related Work

Our combinators have been adapted from those of the Orc [START_REF] Kitchin | A language for task orchestration and its semantic properties[END_REF][START_REF] Kitchin | The Orc programming language[END_REF] programming language. In ParT, these combinators are completely asynchronous and are integrated with futures. ParTs are first class citizens and can be nested Par (Par t), neither of which is possible in Orc, which sits on top of the expression being coordinated and a flat collection of values.

Meseguer et al. [START_REF] Alturki | Dist-Orc: A rewriting-based distributed implementation of Orc with formal analysis[END_REF] used rewriting logic semantics and Maude to provide a distributed implementation of Orc. Their focus on the semantic model allows them to model check Orc programs. In this paper, our semantics is more finegrained, and guides the implementation in a multicore setting.

ParT uses a monad to encapsulate asynchronous computations, which is not a new idea [START_REF] Devesas | Implementation of an orchestration language as a Haskell domain specific language[END_REF][START_REF] Launchbury | Concurrent orchestration in Haskell[END_REF][START_REF] Syme | The F# asynchronous programming model[END_REF]. For instance, F# expresses asynchronous workflows using a continuation monad [START_REF] Syme | The F# asynchronous programming model[END_REF] but cannot create more parallelism within the monad, making the model better suited for event-based programming. In contrast, our approach can spawn parallel computations and include them within ParTs.

Other work implements Orc combinators in terms of a monad within the pure functional language Haskell [START_REF] Devesas | Implementation of an orchestration language as a Haskell domain specific language[END_REF][START_REF] Launchbury | Concurrent orchestration in Haskell[END_REF]. One of these approaches [START_REF] Devesas | Implementation of an orchestration language as a Haskell domain specific language[END_REF] relies on threads and channels and implements the prune combinator using sequential composition, losing potential parallelism. The other approach [START_REF] Launchbury | Concurrent orchestration in Haskell[END_REF] uses Haskell threads and continuations to model parallel computations and re-designs the prune combinator in terms of a cut combinator thats sparks off parallel computations, waits until there is a value available and terminates, in bulk, the remaining computations. In contrast, the ParT abstraction relies on more lightweight tasks instead of threads, has fully asynchronous combinators, which maintain the throughput of the system, and terminates speculative work by recursively poisoning dependencies and terminating computations that are not needed.

An approach to increase parallelism is to create parallel versions of existing collections. For instance, Haskell [START_REF] Simon | Harnessing the multicores: Nested data parallelism in Haskell[END_REF] adds parallel operations to its collections, and the Scala parallel collections [START_REF] Prokopec | A generic parallel collection framework[END_REF] adds new methods to their collection, par and seq, that return a parallel and a sequential version of the collection. However these approaches cannot coordinate complex workflows, which is possible with the ParT abstraction.

Recent approaches to creating pipeline parallelism are the Flowpool [START_REF] Prokopec | Flowpools: A lock-free deterministic concurrent dataflow abstraction[END_REF] and FlumeJava [START_REF] Chambers | Flumejava: Easy, efficient data-parallel pipelines[END_REF] abstractions. In the former, functions are attached to Flowpool and, with the foreach combinator, the attached functions are applied to items asynchronously added to the Flowpool thereby creating parallel pipelines of computations. The latter, FlumeJava, is a library extending the MapReduce framework; it provides high-level constructs to create efficient data-parallel pipelines of MapReduce jobs, via an optimisation phase. The ParT abstraction can create data-parallel pipelines with the sequence and bind = combinators (at the moment there is no optimisation phase) and further can terminate speculative work.

Existing approaches to safely terminating speculative parallelism [START_REF] Frigo | The implementation of the Cilk-5 multithreaded language[END_REF][START_REF] Imam | The Eureka programming model for speculative task parallelism[END_REF][START_REF] Peierls | Java Concurrency in Practice[END_REF] did not integrate well with the ParT abstraction. For instance, the Cilk programming language provides the abort keyword to terminate all speculative work generated by a procedure [START_REF] Frigo | The implementation of the Cilk-5 multithreaded language[END_REF]. The termination does not happen immediately, instead, computations are marked as not-runnable; already running computations would get marked as non-runnable but do not stop execution until their work is finished. In other approaches, the developer specifies termination checkpoints at which a task may be terminated [START_REF] Imam | The Eureka programming model for speculative task parallelism[END_REF][START_REF] Peierls | Java Concurrency in Practice[END_REF]. This solves the previous problem and improves responsiveness but, adds an extra overhead (for the checking) and puts the responsibility on the developer, who specifies the location of the checkpoints. In our design, the developer does not need to specify these checkpoints and speculative work is terminated as soon as there are no dependencies. No other approach considers that the results of tasks may be needed elsewhere.

Conclusion and Future Work

This paper presented the ParT asynchronous, parallel collection abstraction, and a collection of combinators that operate over it. ParT was formalised as a typed calculus of tasks, futures and Orc-like combinators. A primary characteristic of the calculus is that it captures the non-blocking implementation of the combinators, including an algorithm for pruning that tracks down dependencies and is safe with respect to shared futures. The ParT abstraction has prototypes in the Encore (statically typed) and Clojure (dynamically typed) programming languages.

Currently, the calculus does not support side-effects. These are challenging to deal with, due to potential race conditions and terminated computations leaving objects in an inconsistent state. We expect that Encore's capability type system [START_REF] Brandauer | Parallel objects for multicores: A glimpse at the parallel language Encore[END_REF] can be used to avoid data races, and a run-time, transactional mechanism can deal with the inconsistent state. At the start of the paper we mentioned that ParT was integrated into an actor-based language, but the formalism included no actors. This work abstracted away the actors, replacing them by tasks and futures-message sends in the Encore programming language return results via futures-which were crucial for tying together the asynchronous computations underlying a ParT. Actors can easily be re-added as soon as the issues of shared mutable state have been addressed. The distribution aspect of actors has not yet been considered in Encore or in the ParT abstraction. This would be an interesting topic for future work. Beyond these extensions, we also plan to extend the range of combinators supporting the ParT abstraction.

eFig. 2 :

 2 Fig. 2: Syntax of the language.

  let x = e in e = (λx.e ) e e 1 > < e 2 = let x = e 1 in (λy.(y (λz.match z with Nothing → e 2 ; → x)) † ) x e 1 = e 2 = join (e 1 e 2 ) maybe2par = λx.match x with Nothing → {}; Just y → {y}

Fig. 3 :

 3 Fig. 3: Runtime configurations.

Fig. 6 :

 6 Fig. 6: Reduction rules for the sequence combinator.

  deps({e}) = deps(λx .e) = deps(async e) = deps(e • ) = deps(e † ) = deps(peek π e) = deps(join e) = deps(e) deps(e || e ) = deps(e e ) = deps(e e ) = deps(e = e ) = deps(e > < e ) = deps(e e ) = deps(e e ) = deps(e) ∪ deps(e ) deps((task α f e)) = deps(e) deps((chain α f g e)) = {g} ∪ deps(e).

Fig. 10 :

 10 Fig. 10: Poisoning reduction rules.

Fig. 11 :Fig. 12 :

 1112 Fig. 11: Safely poisoning and terminating a configuration. The letter in the top right corner indicates the order. Tasks are represented by squares, contain a body and have an arrow to the future they write to. Futures (circles) have dotted arrows to tasks that use them. Grey represents poisoned configurations. Terminated configurations are removed.

Fig. 14 :

 14 Fig. 14: Expression Typing.

Fig. 15 :

 15 Fig. 15: Configuration Typing.

The monad operations on Par are essentially the same as for lists but parallelised.

Γ ρ e1 e2 : τ (TS-Fun) Γ, x : τ ρ e : τ Γ ρ λx.e : τ → τ (TS-Async) Γ ρ e : τ Γ ρ async e : Fut τ (TS-Chain) Γ ρ e1 : Fut τ Γ ρ e2 : τ → τ Γ ρ e1 e2 : Fut τ (TS-EmptyPar) Γ ρ {} : Par τ (TS-SingletonPar) Γ ρ e : τ Γ ρ {e} : Par τ (TS-LiftF) Γ ρ e : Fut τ Γ ρ e • : Par τ (TS-LiftFP) Γ ρ e : Fut (Par τ ) Γ ρ e † : Par τ (TS-Par) Γ ρ e1 : Par τ Γ ρ e2 : Par τ Γ ρ e1 || e2 : Par τ (TS-Sequence) Γ ρ e1 : Par τ Γ ρ e2 : τ → τ Γ ρ e1 e2 : Par τ (TS-Join) Γ ρ e : Par (Par τ ) Γ ρ join e : Par τ (TS-Otherwise) Γ ρ e1 : Par τ Γ ρ e2 : Par τ Γ ρ e1 > < e2 : Par τ (TS-Peek) Γ Maybe ρ e : Par ρ Γ Maybe ρ peek π e : τ (TS-Prune) Γ ρ e1 : Fut (Maybe τ ) → Par τ Γ ρ e2 : Par τ Γ ρ e1 e2 : Par τ

Encore ParT prototype: http://52.50.101.143/kompile/encore/

Clojure ParT prototype: https://github.com/kikofernandez/ParT

Partly funded by the EU project FP7-612985 UpScale: From


Lian Xuan

Lei Xuefeng

Xiao Guanyu

Liang Yang

Heat Transfer effects on Auto-Ignition behavior of Natural Gas and Heptane Fueled HCCI combustion: a Multi-Zone Simulation

Keywords: HCCI Combustion, Natural Gas, Heptane, Heat Transfer, Detailed Chemical Kinetics

The Homogenous Charge Compression Ignition (HCCI) combustion in an natural gas (Methane) and Heptane fueled engine using detailed chemical kinetics is investigated in this research. Sensitivity analysis of O, H, CH and OH species have been performed for the two sample fuels. The effect of heat transfer of start of combustion (SOC) and temperature gradient have been investigated.

The SOC shifts to the higher crank angles as the heat transfer is considered because of the heat loss to the cylinder body and later combustion is happening inside the cylinder.

Introduction

Very low NOx and almost no soot emissions and elevated thermodynamic efficiency, made Homogenous Charge Compression Ignition (HCCI) combustion a great candidate combustion methods for next generations of internal combustion engines [START_REF] Nobakht | A parametric study on natural gas fueled hcci combustion engine using a multi-zone combustion model[END_REF][START_REF] Onishi | Active thermo-atmosphere combustion (atac)-a new combustion process for internal combustion engines[END_REF][START_REF] Najt | Compression-ignited homogeneous charge combustion[END_REF][START_REF] Maurya | Numerical investigation of ethanol fuelled hcci engine using stochastic reactor model. part 2: Parametric study of performance and emissions characteristics using new reduced ethanol oxidation mechanism[END_REF][START_REF] Nobakht | Optimization of gri-mech 3.0 mechanism using hcci combustion models and genetic algorithm[END_REF][START_REF] Mahabadipour | A second law-based framework to identify high efficiency pathways in dual fuel low temperature combustion[END_REF][START_REF] Mahabadipour | lost available imep: A second-law-based performance parameter for ic engines[END_REF]. The most benefits of HCCI combustion is because 5 of its premixed and lean fast combustion. Large heat release rate (HRR) with a combustion without a flame front [START_REF] Eng | The effect of pox on the autoignition chemistry of n-heptane and isooctane in an hcci engine[END_REF]. The high thermal efficiency of HCCI combustion is due to its ability to design for high compression ratios (CR), lean and almost constant volume combustion with no throttle loss, [START_REF] Yang | Development of a gasoline engine system using hcci technology-the concept and the test results[END_REF][START_REF] Mahabadipour | Characterization of exhaust exergy flows in a diesel engine from the perspective of exhaust waste energy recovery[END_REF].

There are some obstacles need to be overcome to commercialize the HCCI engines with these great features. Difficulties in cold start and high HC and CO emissions, and small range of normal operating for HCCI engines are some of the difficulties [START_REF] Eng | Characterization of pressure waves in hcci combustion[END_REF][START_REF] Nobakht | Cfd simulation of tesla-type microvalves[END_REF]. One of the challenges for HCCI engine design is controlling the start of ignition for different speed and operational load operating conditions of the engine [START_REF] Zheng | Charge stratification to control hcci: Experiments and cfd modeling with n-heptane as fuel[END_REF]. So, simulations based on parametric study to approach a reliable control method of HCCI combustion currently is highly demanding by the scientists and engineers [START_REF] Lu | A fundamental study on the control of the hcci combustion and emissions by fuel design concept combined with controllable egr. part 2. effect of operating conditions and egr on hcci combustion[END_REF][START_REF] Komninos | A parametric investigation of hydrogen hcci combustion using a multi-zone model approach[END_REF]. Some examples of methods used to control HCCI combustion, are inlet pressure and temperature changes and altering the compression ratio (VVT method) [START_REF] Zheng | Use of a single-zone thermodynamic model with detailed chemistry to study a natural gas fueled homogeneous charge compression ignition engine[END_REF][START_REF] Haraldsson | Hcci combustion phasing in a multi cylinder engine using variable compression ratio[END_REF].

In order to design an engine which uses HCCI combustion and is reliable for use, controlling is vital to understand the effects of altering each engine and combustion parameter change on HCCI combustion output and behavior. For this purpose, in this research we have performed a study to investigate effects of altering each parameter on HCCI engine combusiton to understand effect of inlet pressure, inlet temperature, air fuel ratio, cylinder compression, and engine speed on in-cylinder pressure history, start of combustionof a Natural Gas and Heptane fueled HCCI combustion engines.

Methodology

As shown in Fig. 1, the cylinder is divided to five different zones with different sizes and shapes; Center volume is centered in the cylinder inside charge, which is an inner gas with a shape of another cylinder which is surrounded by an outer zones with concentric shell of gas. The thickness of these shells are t 1 . The outer zones are cylindrically shaped. The boundary layer is modeled in our simulations too, for this purpose, it is assumed that every zone becomes thinner as we go further from the center towards cylinder walls and the value of R shows the fraction of the thickness of the next layer in comparison to the previous one. Values of the center zone volume is 0.3 of total volume of cylinder.

To model detailed chemical kinetics, we have used the GRI-mech 3.0 chemical kinetic mechanism [START_REF] Gardiner | The gri-mechtm model for natural gas combustion and no formation and removal chemistry[END_REF].

Governing equations 40

Thermodynamic properties in zones are uniform and it is assumed that the gas is an ideal gas. We also assumed that the mass inside the cylinder is homogenous at the beginning of the simulation. After that point, mass transfer model between zones is happening to keep the in-cylinder pressure uniform for the combustion chamber:

dm k dt = 0 (1) Nz k=1 m k = m tot (2)
Energy conservation equation is as follows:

m k ck v dT k dt = -m k Ns i=1 U i dY i,k dt -P dV k t + dQ k dt + ṁi-1→i h i-1 - ṁi→i+1 h i (3)
The net rate of species production can be calculated using:

dY i,k dt = ωi,k M W i ρ k (4)
Woschnis correlation [21] is used to simulate thermal transport between zones with changes which for HCCI engines and combustion simulations applications [START_REF] Chang | New heat transfer correlation for an hcci engine derived from measurements 155 of instantaneous surface heat flux[END_REF]. It is used for convective thermal transport modeling inside the cylinder to transfer heat to cylinder wall.

h c (t) = β × Height(t) -0.2 P (t) 0.8 T (t) -0.73 ν(t) 0.8 (5)
Thermal transport among different zones are modeled by a mechanism which is like conduction. So, heat flux of thermal transport will be dependent on the temperature difference of the zones which are neighbor and on the distance as follows:

q = -K tot dT dy (6)
In Eq. 6, the K tot is a conductivity of total flow which is found by Yang and

Martin method [START_REF] Yang | Approximate solutionone-dimensional energy equation for transient, compressible, low mach number turbulent boundary layer flows[END_REF] and is the summation the turbulent and laminar component.

k tot = K l + K t (7)
The ratio of turbulent to laminar component is calculated by the following equation:

K t K l = P r l P r t µ t µ l (8)
Eq. 8 presupposes flows. The viscosity ratio can by calculated by:

µ t µ l = ky + n [1 -exp(-2αky + n ] (9)
and

y + n = u * µ w u 0 ρdy n ( 10
)
here k = 0.44 which is the Von Karman Constant, α = 0.08 and y + n is the distance between the zone center and the wall. The velocity is proportional to engine rpm.

Results and Discussion

65

For sensitivity analysis when the mixture temperature has increased by 100 K, 200 K, and 300K, first corresponding time for 1600K, 1700K and 1800K are obtained: Based on our simulation results (Fig. 15), considering heat transfer have the same effect on the in-cylinder pressure history.

Conclusions

The effects of heat transfer and engine speed on combustion behavior of HCCI combustion engine is investigated and the following conclusions can be derived from this research: -Increasing engine speed (rpm) will cause delay in SOC because of giving less time to the H radials to react with other species and start the combustion inside the cylinder.

Figure 1 :

 1 Figure 1: Zone configuration of MZCM.

  001099 s corresponding to 1600 K the results of sensitivity analysis for O, H, CH and OH are as follow:

Figure 2 :

 2 Figure 2: Sensitivity analysis of O.

Figure 3 :

 3 Figure 3: Sensitivity analysis of H.

6

 6

Figure 4 :

 4 Figure 4: Sensitivity analysis of CH.

Figure 5 :

 5 Figure 5: Sensitivity analysis of OH.

Figure 6 :

 6 Figure 6: Sensitivity analysis of O.

Figure 7 :

 7 Figure 7: Sensitivity analysis of H.

Figure 8 :

 8 Figure 8: Sensitivity analysis of CH.

Figure 9 :

 9 Figure 9: Sensitivity analysis of OH.

Figure 10 :

 10 Figure 10: Sensitivity analysis of O.

Figure 11 :

 11 Figure 11: Sensitivity analysis of H.

Figure 12 :

 12 Figure 12: Sensitivity analysis of CH.

Figure 13 :

 13 Figure 13: Sensitivity analysis of OH.

Fig 14

 14 Fig 14 shows that considering heat transfer will retire the SOC and also will

Figure 14 :

 14 Figure 14: Temperature profile with respect to crank angle degree (CAD).

Figure 15 :

 15 Figure 15: Pressure profile with respect to crank angle degree (CAD).

Figs

  Figs. ?? demonstrate in-cylinder temperature and pressure histories for the

Figure 16 :

 16 Figure 16: Temperature profile with respect to crank angle degree (CAD).

Figure 17 :

 17 Figure 17: Pressure profile with respect to crank angle degree (CAD).

Figs

  Figs. ?? demonstrate in-cylinder temperature and pressure histories for the

Figure 18 :

 18 Figure 18: Temperature profile with respect to crank angle degree (CAD).

Figure 19 :

 19 Figure 19: Pressure profile with respect to crank angle degree (CAD).

90-

  Considering heat transfer in HCCI simulation causes delay in SOC because of energy loss to the cylinder wall.

Table 1 :

 1 Sensitivity analysis of the mixture

-The peak temperature, pressure and also the average temperature and pressure for the expansion stage is reduce. There for we will have smaller engine performance.