**Acknowledgements**

NKN acknowledges viticulture research funding support from the Canadian Agricultural Partnership (CAP) Program, Agriculture and Agri-Food Canada (AAFC) under project no. 2336, 'Influence of cultural practices and climate change on sustainability of grape production under northern conditions'. I thank Dr. T.A. Porcelli for helpful editing and feedback.


P **sat** loopinv(α) ∩ {| α > 0 |}, R, G, ∃β < α. loopinv(β) ∧ loopinv(α) ∩ {| α > 0 |}⊆{| b |} ∧ loopinv(0) ⊆ {| ¬b |}∧∀s ∈ loopinv(α). (s, t) ∈ R −→ ∃β α. t ∈ loopinv(β)

#### **5.2 Correctness Specification**

Using the compositional reasoning of π-Core, correctness of Zephyr memory management can be specified and verified with the rely-guarantee specification of each event. The functional correctness of a kernel service is specified by its pre/post-conditions. Invariant preservation, memory configuration, and separation of local variables is specified in the guarantee condition of each service.

The guarantee condition for both memory services is defined as:

$$\begin{aligned} & \mathbf{Mem-pool-alloc-guard} \mathrel{\mathbf{s} \equiv \overset{(1)}{Id} \cup \overbrace{(gvars.conf.stable \cap } \cap }^{(2)} \\ & \{ (s.r.) . \overbrace{(\text{car } s \neq Sone \, t \longrightarrow gvars - nochange \, s \, r \wedge lvars-nochange \, t \, s \, r \,}^{(3.1)}) \\ & \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \$$

This relation states that *alloc* and *free* services may not change the state (1), e.g., a blocked await or selecting branch on a conditional statement. If it changes the state then: (2) the static configuration of memory pools in the model do not change; (3.1) if the scheduled thread is not the thread invoking the event then variables for that thread do not change (since it is blocked in an *Await* as explained in Sect. 3); (3.2) if it is, then the relation preserves the memory invariant, and consequently each step of the event needs to preserve the invariant; (4) a thread does not change the local variables of other threads.

Using the π-Core proof rules we verify that the invariant introduced in Sect. 4 is preserved by all the events. Additionally, we prove that when starting in a valid memory configuration given by the invariant, then if the service does not returns an error code then it returns a valid memory block with size bigger or equal than the requested capacity. The property is specified by the following postcondition:

**Mem-pool-alloc-pre***t*≡ {*s*.*inv s*∧*allocating-node s t*=*None*∧*freeing-node s t*=*None*} **Mem-pool-alloc-post** *t p sz timeout* ≡

{*s*. *inv s* ∧ *allocating-node s t* = *None* ∧ *freeing-node s t* = *None*

∧ (*timeout* = *FOREVER* −→

(*ret s t* = *ESIZEERR* ∧ *mempoolalloc-ret s t* = *None* ∨

*ret s t* = *OK* ∧ (∃ *mblk*. *mempoolalloc-ret s t* = *Some mblk* ∧ *mblk-valid s p sz mblk*)))

∧ (*timeout* = *NOWAIT* −→

((*ret s t* = *ENOMEM* ∨ *ret s t* = *ESIZEERR*) ∧ *mempoolalloc-ret s t* = *None*) ∨

(*ret s t* = *OK* ∧ (∃ *mblk*. *mempoolalloc-ret s t* = *Some mblk* ∧ *mblk-valid s p sz mblk*)))

∧ (*timeout* > *0* −→

((*ret s t* = *ETIMEOUT* ∨ *ret s t* = *ESIZEERR*) ∧ *mempoolalloc-ret s t* = *None*) ∨ (*ret s t* = *OK* ∧ (∃ *mblk*. *mempoolalloc-ret s t* = *Some mblk* ∧ *mblk-valid s p sz mblk*)))}

If a thread requests a memory block in mode *FOREVER*, it may successfully allocate a valid memory block, or fail (*ESIZEERR*) if the request size is larger than the size of the memory pool. If the thread is requesting a memory pool in mode *NOWAIT*, it may also get the result of *ENOMEM* if there is no available blocks. But if the thread is requesting in mode *TIMEOUT*, it will get the result of *ETIMEOUT* if there is no available blocks in *timeout* milliseconds.

The property is indeed weak since even if the memory has a block able to allocate the requested size before invoking the allocation service, another thread running concurrently may have taken the block first during the execution of the service. For the same reason, the released block may be taken by another concurrent thread before the end of the release services.

#### **5.3 Correctness Proof**

In the π-Core system, verification of a rely-guarantee specification proving a property is carried out by inductively applying the proof rules for each system event and discharging the proof obligations the rules generate. Typically, these proof obligations require to prove stability of the pre- and post-condition to check that changes of the environment preserve them, and to show that a statement modifying a state from the precondition gets a state belonging to the postcondition.

To prove termination of the loop statement in *free block* shown in Fig. 4, we define the loop invariant with the logical variable α as follows.

**mp-free-loopinv** *t b* α ≡ {| *...* ∧´*inv* ∧ *level b* < *length* (´*lsizes t*)

```
∧ (∀ ii<length (´lsizes t). ´lsizes t ! ii = (max-sz (´mem-pool-info (pool b))) div (4 ˆ ii))
```
∧ ´*bn t* < *length* (*bits* (*levels* (´*mem-pool-info* (*pool b*))!(´*lvl t*)))

∧ ´*bn t* = (*block b*) *div* (*4 ˆ* (*level b* − ´*lvl t*)) ∧ ´*lvl t* ≤ *level b*

∧ (´*free-block-r t* −→ (∃ *blk*. ´*freeing-node t* = *Some blk* ∧ *pool blk* = *pool b*

∧ *level blk* = ´*lvl t* ∧ *block blk* = ´*bn t*)

∧ ´*alloc-memblk-data-valid* (*pool b*) (*the* (´*freeing-node t*))) ∧ (¬ ´*free-block-r t* −→ ´*freeing-node t* = *None*) |} ∩ {| α = (*if* ´*freeing-node t* = *None then* ´*lvl t* + *1 else 0*) |}

freeing node and lvt are local variables respectively storing the node being free and the level that the node belongs to. In the body of the loop, if lvl t > 0 and partner bit is *true*, then lvl = lvl − 1 at the end of the body. Otherwise, freeing node t = None. So at the end of the loop body, α decreases or α = 0. If α = 0, we have freeing node t = None, and thus the negation of the loop condition ¬free block r t, concluding termination of *free block*.

Due to concurrency, it is necessary to consider fairness to prove termination of the loop statement in *k mempool alloc* from Line 23 to 33 in Fig. 1. On the one hand, when a thread requests a memory block in the *FOREVER* mode, it is possible that there will never be available blocks since other threads do not release allocated blocks. On the other hand, even when other threads release blocks, it is possible that the available blocks are always raced by threads.

#### **6 Evaluation and Results**

*Evaluation.* The verification conducted in this work is on Zhephyr v1.8.0, released in 2017. The C code of the buddy memory management is ≈400lines, not counting blank lines and comments. Table 1 shows the statistics for the effort and size of the proofs in the Isabelle/HOL theorem prover. In total, the models and mechanized verification consists of ≈28,000 lines of specification and proofs, and the total effort is ≈12 person-months. The specification and proof of π-Core are reusable for the verification of other systems.

**Table 1.** Specification and proof statistics

*Bugs in Zephyr.* During the formal verification, we found 3 bugs in the C code of Zephyr. The first two bugs are critical and have been repaired in the latest release of Zephyr. To avoid the third one, callers to *k mem pool alloc* have to constrain the argument *t size size*.

**(1) Incorrect block split:** this bug is located in the loop in Line 11 of the *k mem pool alloc* service, shown in Fig. 1. The *level empty* function checks if a pool p has blocks in the free list at level *alloc l*. Concurrent threads may release a memory block at that level making the call to *level empty(p, alloc l)* to return *false* and stopping the loop. In such case, it allocates a memory block of a bigger capacity at a level i but it still sets the level number of the block as *alloc l* at Line 15. The service allocates a larger block to the requesting thread causing an internal fragmentation of max sz/4i − max sz/4alloc l bytes. When this block is released, it will be inserted into the free list at level *alloc l*, but not at level i, causing an external fragmentation of max sz/4i − max sz/4alloc l . The bug is fixed by removing the condition *level empty(p, alloc l)* in our specification.

**(2) Incorrect return from** *k mem pool alloc***:** this bug is found at Line 26 in Fig. 1. When a suitable free block is allocated by another thread, the *pool alloc* function returns *EAGAIN* at Line 9 to ask the thread to retry the allocation. When a thread invokes *k mem pool alloc* in *FOREVER* mode and this case happens, the service returns *EAGAIN* immediately. However, a thread invoking *k mem pool alloc* in *FOREVER* mode should keep retrying when it does not succeed. We repair the bug by removing the condition ret == EAGAIN at Line 26. As explained in the comments of the C Code, *EAGAIN* should not be returned to threads invoking the service. Moreover, the *return EAGAIN* at Line 34 is actually the case of time out. Thus, we introduce a new return code *ETIMEOUT* in our specification.

**(3) Non-termination of** *k mem pool alloc***:** we have discussed that the loop statement at Lines 23–33 in Fig. 1 does not terminate. However, it should terminate in certain cases, which are actually violated in the C code. When a thread requests a memory block in *FOREVER* mode and the requested size is larger than *max sz*, the maximum size of blocks, the loop at Lines 23–33 in Fig. 1 never finishes since *pool alloc* always returns *ENOMEM*. The reason is that the "*return ENOMEM* " at Line 6 does not distinguish two cases, alloc l < 0 and free l < 0. In the first case, the requested size is larger than *max sz* and the kernel service should return immediately. In the second case, there are no free blocks larger than the requested size and the service tries forever until some free block available. We repair the bug by splitting the *if* statement at Lines 4–7 into these two cases and introducing a new return code *ESIZEERR* in our specification. Then, we change the condition at Lines 25–26 to check that the returned value is *ESIZEERR* instead of *ENOMEM*.

#### **7 Conclusion and Future Work**

In this paper, we have developed a formal specification at low-level design of the concurrent buddy memory management of Zephyr RTOS. Using the relyguarantee technique in the π-Core framework, we have formally verified a set of critical properties for OS kernels such as invariant preservation, and preservation of memory configuration. Finally, we identified some critical bugs in the C code of Zephyr.

Our work explores the challenges and cost of certifying concurrent OSs for the highest-level assurance. The definition of properties and rely-guarantee relations is complex and the verification task becomes expensive. We used 40 times of LOS/LOP than the C code at low-level design. Next, we are planning to verify other modules of Zephyr, which may be easier due to simpler data structures and algorithms. For the purpose of fully formal verification of OSs at source code level, we will replace the imperative language in π-Core by a more expressive one and add a verification condition generator (VCG) to reduce the cost of the verification.

#### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **Violat: Generating Tests of Observational Refinement for Concurrent Objects**

Michael Emmi1(B) and Constantin Enea2

1 SRI International, New York, NY, USA<EMAIL_ADDRESS>2 Universit´e de Paris, IRIF, CNRS, 75013 Paris, France<EMAIL_ADDRESS>
**Abstract.** High-performance multithreaded software often relies on optimized implementations of common abstract data types (ADTs) like counters, key-value stores, and queues, i.e., *concurrent objects*. By using fine-grained and non-blocking mechanisms for efficient inter-thread synchronization, these implementations are vulnerable to violations of ADTconsistency which are difficult to detect: bugs can depend on specific combinations of method invocations and argument values, as well as rarely-occurring thread interleavings. Even given a bug-triggering interleaving, detection generally requires unintuitive test assertions to capture inconsistent combinations of invocation return values.

In this work we describe the Violat tool for generating tests that witness violations to atomicity, or weaker consistency properties. Violat generates self-contained and efficient programs that test *observational refinement*, i.e., substitutability of a given ADT with a given implementation. Our approach is both sound and complete in the limit: for every consistency violation there is a failed execution of some test program, and every failed test signals an actual consistency violation. In practice we compromise soundness for efficiency via random exploration of test programs, yielding probabilistic soundness instead. Violat's tests reliably expose ADT-consistency violations using off-the-shelf approaches to concurrent test validation, including stress testing and explicit-state model checking.

#### **1 Introduction**

Many mainstream software platforms including Java and .NET support multithreading to enable parallelism and reactivity. Programming multithreaded code effectively is notoriously hard, and prone to data races on shared memory accesses, or deadlocks on the synchronization used to protect accesses. Rather than confronting these difficulties, programmers generally prefer to leverage libraries providing *concurrent objects* [19,29], i.e., optimized thread-safe implementations of common abstract data types (ADTs) like counters, key-value stores, and queues. For instance, Java's concurrent collections include implementations which eschew the synchronization bottlenecks associated with lock-based mutual exclusion, opting instead for non-blocking mechanisms [28] provided by hardware operations like *atomic compare and exchange*.

Concurrent object implementations are themselves vulnerable to elusive bugs: even with effective techniques for exploring the space of thread interleavings, like stress testing or model checking [7,30,47], bugs often depend on specific combinations of method invocations and argument values. Furthermore, even recognizing whether a given execution is *correct* is non-trivial, since recognition generally requires unintuitive test assertions to identify inconsistent combinations of return values. Technically, correctness amounts to *observational refinement* [18,21,32], which captures the substitutability of an ADT with an implementation [23]: any combination of values admitted by a given implementation is also admitted by the given ADT specification.

In this work we describe an approach to generating tests of observational refinement for concurrent objects, as implemented by the Violat tool, which we use to discover violations to atomicity (and weaker consistency properties) in widely-used concurrent objects [9,10,12]. Unlike previous approaches based on *linearizability* [4,20,46], Violat generates self-contained test programs which do not require enumerating linearizations dynamically *per execution*, instead statically precomputing the ADT-admitted return-value outcomes *per test program*, once, prior to testing. Despite this optimization, the approach is both sound and complete, i.e., in the limit: for every consistency violation there is a failed execution of some test program, and every failed test witnesses an actual consistency violation. In practice, we compromise soundness for efficiency via random exploration of test programs, achieving probabilistic soundness instead.

Besides improving the efficiency of test execution, Violat's self-contained tests can be validated by both stress testers and model checkers, and double as regression and conformance tests. Our previous works [9,10,12] demonstrate that Violat's tests reliably expose ADT-consistency violations in Java implementations using the Java Concurrency Stress testing tool [42]. In particular, Violat has uncovered atomicity violations in over 50 methods from Java's concurrent collections; many of these violations seem to correspond with their documentations' mention of *weakly-consistent* behavior, while others indicate confirmed implementation bugs, which we have reported.

Previous work used Violat in empirical studies, without artifact evaluation [9,10,12]. This article is the first to consider Violat itself for evaluation, the first to describe its implementation and usage, and includes several novel extensions. For instance, in addition to stress testing, Violat now includes an integration with Java Pathfinder [47]; besides enabling complete systematic coverage of a given test program, this integration enables the output of the execution traces leading to consistency violations, thus facilitating diagnosis and repair. Furthermore, Violat is now capable of generating tests of any user-provided implementation, in addition to those distributed with Java.

#### **2 Overview of Test Generation with Violat**

Violat generates self-contained programs to test the observational refinement of a given concurrent object implementation with respect to its abstract data type (ADT), according to Fig. 1. While its methodology is fairly platform agnostic, Violat currently integrates with the Java platform. Accordingly, its input includes the fully-qualified name of a single Java class, which is assumed to be available either on the system classpath, or in a user-provided Java archive (JAR); its output is a sequence of Java classes which can be tested with offthe-shelf back-end analysis engines, including the Java Concurrency Stress testing tool [42] and Java Pathfinder [47]. Our current implementation integrates directly with both back-ends, and thus reports test results directly, signaling any discovered consistency violations.

**Fig. 1.** Violat generates tests by enumerating program schemas invoking a given concurrent object, annotating those schemas with the expected outcomes of invocations according to ADT specifications, and translating annotated schemas to executable tests.

Violat generates tests according to a three-step pipeline. The first step, described in Sect. 3, enumerates test program *schemas*, i.e., concise descriptions of programs as parallel sequences of invocations of the given concurrent object's methods. For example, Fig. 2 lists several test schemas for Java's ConcurrentHashMap. The second step, described in Sect. 4, annotates each schema with a set of expected *outcomes*, i.e., the combinations of return values among the given schema's invocations which are admitted according to the given object's ADT specification. The final step, described in Sect. 5, translates each schema into a self-contained1 Java class.

Technically, to guide the enumeration of schemas and calculation of outcomes, Violat requires a specification of the given concurrent object, describing constructor and method signatures. While this could be generated automatically from the object's bytecode, our current implementation asks the user to input this specification in JSON format. By additionally indicating whether methods are read-only or weakly-consistent, the user can provide additional hints to

1 The generated class imports only a given concurrent object, and a few basic java.util classes.

improve schema enumeration and outcome calculation. For instance, excessive generation of programs with only read-only methods is unlikely to uncover consistency violations, and weakly-consistent ADT methods generally allow additional outcomes – see Emmi and Enea [12]. Furthermore, Violat attempts to focus the blame for discovered violations by constructing tests with a small number of specified *untrusted* methods, e.g., just one.

#### **3 Test Enumeration**

To enumerate test programs effectively, Violat considers a simple representation of program *schemas*, as depicted in Fig. 2. We write schemas with a familiar notation, as parallel compositions *{*...*}*||*{*...*}* of method-invocation sequences. Intuitively, schemas capture parallel threads invoking sequences of methods of a given concurrent object. Besides the parallelism, these schemas include only trivial control and data flow. For instance, we exclude conditional statements and loops, as well as passing return values as arguments, in favor of straight-line code with literal argument values. Nevertheless, this simple notion is expressive enough to capture any possible *outcome*, i.e., combination of invocation return values, of programs with arbitrarily complex control flow, data flow, and synchronization. To see this, consider any outcome *y* admitted by some execution of a program with arbitrarily-complex control and data flow in which methods are invoked with argument values *x*, collectively. The schema in which each thread invokes the same methods of a thread of the original program with literal values *x*, collectively, is guaranteed to admit the same outcome *y*.

**Fig. 2.** Program schemas generated by Violat for Java's ConcurrentHashMap class, along with outcomes which are observed in testing, yet not predicated by Violat.

For a given concurrent object, Violat enumerates schemas according to a few configurable parameters, including bounds on the number of threads, invocations, and (primitive) values. By default, Violat generates schemas with exactly 2 threads, between 3 and 6 invocations, and exactly 2 values. While our initial implementation enumerated schemas systematically according to a welldefined order, empirically we found that this strategy spends too much time in neighborhoods of uninteresting schemas, i.e., which do not expose violations. Ultimately we adopted a pseudorandom enumeration which constructs each schema independently by randomly choosing the number of threads, invocations, and values, within the given parameter bounds, and randomly populating threads with invocations. Methods are selected according to a weighted random choice, in which the weights of read-only and untrusted methods is 1; trusted mutator methods have weight 3. The read-only and trusted designations are provided by class specifications – see Sect. 2. Integer argument values are chosen randomly between 0 and 1, according to the default value bound; generic-typed arguments are assumed to be integers. Collection and map values are constructed from randomly-chosen integer values, up to size 2. In principle, all of these bounds are configurable, but we have found these defaults to work reasonably well.

Note that while the manifestation of a given concurrency bug can, in principle, rely on large bounds on threads, invocations, and values, recent studies demonstrate that the majority (96%) can be reproduced with just 2 threads [25]. Furthermore, while our current implementation adheres to the simple notion of schema in which all threads are execute in parallel, Violat can easily be extended to handle a more complex notion of schema in which threads are partially ordered, thus capturing arbitrary program synchronization. Nevertheless, this simple notion seems effective at exposing violations without requiring additional synchronization – see Emmi and Enea [12, Section 5.2].

#### **4 Computing Expected Outcomes**

To capture violations to observational refinement, Violat computes the set of *expected outcomes*, i.e., those admitted by a given concurrent object's abstract data type (ADT), for each program schema. Violat essentially follows the approach of Line-Up [4] by computing expected outcomes from sequential executions of the given implementation. While this approach assumes that the sequential behavior of a given implementation does adhere to its implicit ADT specification – and that the outcomes of concurrent executions are also outcomes of sequential executions – there is typically no practical alternative, since behavioral ADT specifications are rarely provided.

Violat computes the expected outcomes of a given schema once, by enumerating all possible shuffles of threads' invocations, and recording the return values of each shuffle when executed by the given implementation. For instance, there are 10 ways to shuffle the threads of the schema

*{* get(1); containsValue(1) *}* || *{* put(1,1); put(0,1); put(1,0) *}*

from Fig. 2, including the sequence

get(1); put(1,1); put(0,1); put(1,0); containsValue(1).

Executing Java's ConcurrentHashMap on this shuffle yields the values null, null, null, 1, and true, respectively. To construct the generated outcome, Violat reorders the return values according to the textual order of their corresponding invocations in the given schema; since containsValue is second in this order, after get, the generated outcome is null, true, null, null, 1. Among the 10 possible shuffles of this schema, there are only four unique outcomes – shown later in Figs. 3 and 4.

**Fig. 3.** Code generated for the containsValue schema of Fig. 2 for Java Pathfinder. Code generation for jcstress similar, but conforms to the tool's idiomatic test format using decorators, and built-in thread and outcome management.

Note that in contrast to existing approaches based on *linearizability* [20], including Line-Up [4], which enumerate linearizations *per execution* of a given program, Violat only enumerates linearizations once *per schema*. This is made possible for two reasons. First, by considering simple test programs in which all invocations are known *statically*, we know the precise set of invocations (including argument values) to linearize even before executing the program. Second, according to sequential happens-before consistency [12], we consider the recording of real-time ordering among invocations infeasible on modern platforms like Java and C++11, which provide only weak ordering guarantees according to a platform-defined happens-before relation. This enables the static prediction of ordering constraints among invocations. While this static enumeration is also exponential in the number of invocations, it becomes an additive rather than multiplicative factor, amounting to significant performance gains in testing.

**Fig. 4.** Observed outcomes for the size method, recorded by Java Pathfinder and jcstress. Outcomes list return values in program-text order, e.g., get's return value is listed first.

#### **5 Code Generation and Back-End Integrations**

Once schemas are annotated with expected outcomes, the translation to actual test programs is fairly straightforward. Note that until this point, Violat is mainly agnostic to the underlying platform for which tests are being generated. The only exception is in computing the expected outcomes for schema linearizations, which executes the given concurrent object implementation as a stand-in oracle for its implicit ADT specification.

Figure 3 lists a simplification of the code generated for the containsValue schema of Fig. 2. The test program initializes a concurrent-object instance and a hash table of expected outcomes, then runs the schema's threads in parallel, recording the results of each invocation, and checks, after threads complete, whether the recorded outcome is expected. To avoid added inter-thread interference and the masking of potential weak-memory effects, each recorded result is isolated to a distinct cache line via Java's *contended* decorator. The actual generated code also includes exception handling, elided here for brevity.

Our current implementation of Violat integrates with two analysis back-ends: the Java Concurrency Stress testing tool [42] (jcstress) and Java Pathfinder [47]. Figure 4 demonstrates the results of each tool on the code generated from the containsValue schema of Fig. 2. Each tool observes executions with the 4 expected outcomes, as well as executions yielding an outcome that Violat does not predict, thus signaling a violation to observational refinement (and atomicity). Java Pathfinder explores 18 program paths in a few seconds – achieving exhaustiveness via partial-order reduction [16] – while jcstress explores nearly 4 million executions in 1 s, observing the unpredicted outcome only twice. Aside from this example, Violat has uncovered consistency violations in over 50 methods of Java's concurrent collections [9,10,12].

#### **6 Usage**

Violat is implemented as a Node.js command-line application, available from GitHub and npm.2 Its basic functionality is provided by the command:

```
$ violat-validator ConcurrentHashMap.json
...
violation discovered
{ put(0,1); size(); contains(1) } || { put(0,0); put(1,1) }
outcome OK frequency
0, 0, true, null, null X 7
0, 1, true, null, null -
                        703
0, 2, true, null, null -
                        94,636
null, 1, false, 1, null -
                        2,263
null, 1, true, 1, null -
                        59,917
null, 2, true, 1, null -
                        4
...
```
reporting violations among 100 generated programs. User-provided classes, individual schemas, program limits, and particular back-ends can also be specified:

```
$ violat-validator MyConcurrentHashMap.json \
```
A full selection of parameters is available from the usage instructions:

```
$ violat-validator --help
```
#### **7 Related Work**

Terragni and Pezz`a survey several works on test generation for concurrent objects [45]. Like Violat, Ballerina [31] and ConTeGe [33] enumerate tests randomly, while ConSuite [43], AutoConTest [44], and CovCon [6] exploit static analysis to compute potential shared-memory access conflicts to reduce redundancy among generated tests. Similarly, Omen [35–38], Narada [40], Intruder [39], and Minion [41] reduce redundancy by anticipating potential concurrency faults during sequential execution. Ballerina [31] and ConTeGe [33] compute linearizations, but only identify generic faults like data races, deadlocks, and exceptions, being neither sound nor complete for testing observational refinement: fault-free executions with un-admitted return-value combinations are false negatives, while faulting executions with admitted return-value combinations are generally false positives – many non-blocking concurrent objects exhibit

2 https://github.com/michael-emmi/violat.

data races by design. We consider the key innovations of these works, i.e., redundancy elimination, orthogonal and complementary to ours. While Pradel and Gross do consider subclass substitutability [34], they only consider programs with two concurrent invocations, and require exhaustive enumeration of the superclass's thread interleavings to calculate admitted outcomes. In contrast, Violat computes expected outcomes without interleaving method implementations, i.e., considering them atomic.

Others generate tests for memory consistency. TSOtool [17] generates random tests against the total-store order (TSO) model, while LCHECK [5] employs genetic algorithms. Mador-Haim et al. [26,27] generate litmus tests to distinguish several memory models, including TSO, partial-store order (PSO), relaxedmemory order (RMO), and sequential consistency (SC). CppMem [2] considers the C++ memory model, while Herd [1] considers release-acquire (RA) and Power in addition to the aforementioned models. McVerSi [8] employs genetic algorithms to enhance test coverage, while Wickerson et al. [48] leverage the Alloy model finder [22]. In some sense, these works generate tests of observational refinement for platforms implementing memory-system ADTs, i.e., with read and write operations, whereas Violat targets arbitrary ADTs, including collections with arbitrarily-rich sets of operations.

Violat more closely follows work on *linearizability* checking. Herlihy and Wing [20] established the soundness of linearizability for observational refinement, and Filipovic et al. [14] established completeness. Wing and Gong [49] developed a linearizability-checking algorithm, which was later adopted by Line-Up [4] and optimized by Lowe [24]; while Violat pays the exponential cost of enumerating linearizations once *per program*, these approaches pay that cost *per execution* – an exponential quantity itself. Gibbons and Korach [15] established NP-hardness of per-execution linearizability checking for arbitrary objects, while Emmi and Enea [11] demonstrate tractability for collections. Bouajjani et al. [3] propose polynomial-time approximations, and Emmi et al. [13] demonstrate efficient symbolic algorithms. Finally, Emmi and Enea [9,10,12] apply Violat to checking atomicity and weak-consistency of Java concurrent objects.

**Acknowledgement.** This work is supported in part by the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant No. 678177).

#### **References**

terdam, The Netherlands, 30 October–4 November 2016, pp. 430–446. ACM (2016). https://doi.org/10.1145/2983990.2984040

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

#### Author Index

Albarghouthi, Aws I-278 André, Étienne I-520 Arcaini, Paolo I-401 Arcak, Murat I-591 Arechiga, Nikos II-137 Ashok, Pranav I-497 Avni, Guy I-630

Backes, John II-231 Bansal, Suguman I-60 Barbosa, Haniel II-74 Barrett, Clark I-443, II-23, II-74, II-116 Bayless, Sam II-231 Becker, Heiko II-155 Beckett, Ryan II-305 Beillahi, Sidi Mohamed II-286 Berkovits, Idan II-245 Biswas, Ranadeep II-324 Bloem, Roderick I-630 Bouajjani, Ahmed II-267, II-286 Brain, Martin II-116 Breck, Jason I-335 Busatto-Gaston, Damien I-572

Černý, Pavol I-140 Češka, Milan I-475 Chatterjee, Krishnendu I-630 Chen, Mingshuai I-650 Cimatti, Alessandro I-376 Coenen, Norine I-121 Cook, Byron II-231 Cyphert, John I-335

D'Antoni, Loris I-3, I-278, I-335 Damian, Andrei II-344 Darulova, Eva II-155, II-174 Davis, Jennifer A. I-366 Deshmukh, Jyotirmoy II-137 Dill, David L. I-443 Dimitrova, Rayna I-241 Dodge, Catherine II-231 Drăgoi, Cezara II-344

Dreossi, Tommaso I-432 Drews, Samuel I-278

Elfar, Mahmoud I-180 Emmi, Michael II-324, II-534 Enea, Constantin II-267, II-286, II-324, II-534 Ernst, Gidon II-208 Erradi, Mohammed II-267

Farzan, Azadeh I-200 Faymonville, Peter I-421 Fedyukovich, Grigory I-259 Feldman, Yotam M. Y. II-405 Feng, Shenghua I-650 Ferreira, Tiago I-3 Finkbeiner, Bernd I-121, I-241, I-421, I-609 Fränzle, Martin I-650 Fremont, Daniel J. I-432 Frohn, Florian II-426 Furbach, Florian I-355

Gacek, Andrew II-231 Ganesh, Vijay II-367 Gao, Sicun II-137 García Soto, Miriam I-297 Gastin, Paul I-41 Gavrilenko, Natalia I-355 Ghosh, Shromona I-432 Giannarakis, Nick II-305 Giesl, Jürgen II-426 Gomes, Victor B. F. I-387 Griggio, Alberto I-376 Guo, Xiaojie II-496 Gupta, Aarti I-259 Gurfinkel, Arie I-161, II-367

Hasuo, Ichiro I-401, I-520 Heljanko, Keijo I-355 Henzinger, Thomas A. I-297, I-630 Hong, Chih-Duo I-455 Hu, Alan J. II-231 Hu, Qinheping I-335

Huang, Derek A. I-443 Humphrey, Laura R. I-366 Hur, Chung-Kil II-445 Ibeling, Duligur I-443 Iosif, Radu II-43 Jagannathan, Suresh II-459 Jain, Mitesh I-553 Jon á š, Martin II-64 Julian, Kyle I-443 Kahsai, Temesghen II-231 Kang, Eunsuk I-219 Kapinski, James II-137 Katz, Guy I-443 Kim, Edward I-432 Kim, Eric S. I-591 Kincaid, Zachary II-97 Kingston, Derek B. I-366 Klein, Felix I-609 Kochenderfer, Mykel J. I-443 Kocik, Bill II-231 Kölbl, Martin I-79 Kong, Soonho II-137 Könighofer, Bettina I-630 Kotelnikov, Evgenii II-231 Křetínský, Jan I-475, I-497 Kukovec, Jure II-231 Lafortune, St éphane I-219 Lal, Akash II-386 Lange, Julien I-97 Lau, Stella I-387 Lazarus, Christopher I-443 Lazi ć, Marijana II-245 Lee, Juneyoung II-445 Lesourd, Maxime II-496 Leue, Stefan I-79 Li, Jianwen II-3 Li, Yangjia II-187 Lim, Rachel I-443 Lin, Anthony W. I-455 Liu, Junyi II-187 Liu, Mengqi II-496 Liu, Peizun II-386 Liu, Tao II-187 Lopes, Nuno P. II-445 Losa, Giuliano II-245

Madhukar, Kumar I-259 Madsen, Curtis I-540 Magnago, Enrico I-376 Mahajan, Ratul II-305 Majumdar, Rupak I-455 Manolios, Panagiotis I-553 Markey, Nicolas I-22 McLaughlin, Sean II-231 Memarian, Kayvan I-387 Meyer, Roland I-355 Militaru, Alexandru II-344 Millstein, Todd I-315 Monmege, Benjamin I-572 Mukherjee, Sayan I-41 Murray, Toby II-208 Myers, Chris J. I-540 Myreen, Magnus O. II-155

Nagar, Kartik II-459 Neupane, Thakur I-540 Niemetz, Aina II-116 Nori, Aditya I-315 Nötzli, Andres II-23 , II-74

Padhi, Saswat I-315 Padon, Oded II-245 Pajic, Miroslav I-180 Pichon-Pharabod, Jean I-387 Piskac, Ruzica I-609 Ponce-de-Le ón, Hern á n I-355 Prabhu, Sumanth I-259 Pranger, Stefan I-630 Preiner, Mathias II-116

Rabe, Markus N. II-84 Ravanbakhsh, Hadi I-432 Reed, Jason II-231 Reps, Thomas I-335 Reynier, Pierre-Alain I-572 Reynolds, Andrew II-23 , II-74 , II-116 Rieg, Lionel II-496 Roohi, Nima II-137 Roussanaly, Victor I-22 Roveri, Marco I-376 Rozier, Kristin Y. II-3 Rümmer, Philipp I-455 Rungta, Neha II-231

Sagiv, Mooly II-405 Sammartino, Matteo I-3 Sanán, David II-515 Sánchez, César I-121 Sankur, Ocan I-22, I-572 Santolucito, Mark I-609 Schilling, Christian I-297 Schledjewski, Malte I-421 Schwenger, Maximilian I-421 Seshia, Sanjit A. I-432, I-591 Sewell, Peter I-387 Shah, Parth I-443 Shao, Zhong II-496 Sharma, Rahul I-315 Shemer, Ron I-161 Shoham, Sharon I-161, II-245, II-405 Siegel, Stephen F. II-478 Silva, Alexandra I-3 Silverman, Jake II-97 Sizemore, John II-231 Solar-Lezama, Armando II-137 Srinivasan, Preethi II-231 Srivathsan, B.  I-60, II-3 Varming, Carsten II-231 Vazquez-Chanlatte, Marcell I-432 Vediramana Krishnan, Hari Govind II-367 Vizel, Yakir I-161, II-367 Volkova, Anastasia II-174

Waga, Masaki I-520 Wahl, Thomas II-386 Walker, David II-305 Wang, Shuling II-187 Wang, Yu I-180 Weininger, Maximilian I-497 Whaley, Blake II-231 Widder, Josef II-344 Wies, Thomas I-79 Wilcox, James R. II-405 Wu, Haoze I-443

Xu, Xiao II-43 Xue, Bai I-650

Ying, Mingsheng II-187 Ying, Shenggang II-187 Yoshida, Nobuko I-97

Zeleznik, Luka I-297 Zeljić, Aleksandar I-443 Zennou, Rachid II-267 Zhan, Bohua II-187 Zhan, Naijun I-650, II-187 Zhang, Zhen I-540 Zhang, Zhenya I-401 Zhao, Yongwang II-515 Zheng, Hao I-540


**2. Methodology**

Perspectives on preschool education and care were reviewed and analysed using a qualitative research technique. Through academic resources, including ERIC, JSTOR, Google Scholar and EBSCOhost, pertinent papers, books and reports were found using a systematic review methodology [2]. Preschool education, early childhood education, play-based learning, curriculum and evaluation, teacher and carer responsibilities, family participation and quality standards were some of the search phrases used. Publications focusing on perspectives, strategies or tactics associated with preschool education and care met the inclusion requirements. Publications with a primary or secondary school theme were excluded.

A total of 59 papers were chosen for examination after the screening. A theme analysis method was used to read the publications and code them. The categories and subcategories formed from the codes were honed after recurrent analysis [2]. Among the types were historical views, preschool education paradigms, philosophical and methodological underpinnings, curriculum and assessment, responsibilities of teachers and carers, parental engagement, quality standards, possibilities and difficulties and future orientations.

The study included locating patterns, trends, and gaps in the literature and analysing [3] the benefits and drawbacks of various methods and procedures. The results were presented utilising important topics and ideas. The study's limitations included the possibility of bias in the choice and analysis of publications and the constrained breadth of the literature review. Yet, the study offers a thorough summary of the state-of-the-art regarding various perspectives on preschool education and care.

### **3. Importance of early childhood education and care**

Early childhood education and care (ECEC) are a critical phase in a child's development [4]. Research shows that providing quality preschool education and care can have numerous benefits. Quality ECEC programmes provide children with opportunities to explore, experiment and develop their skills in a safe and supportive environment, helping them to achieve academic, social and emotional success. One of the most significant benefits of quality preschool education and care is improved educational outcomes. Siraj et al. [5] contend that Children who attend quality ECEC programmes have better literacy, numeracy, and cognitive skills than those who do not. This is because quality ECEC programmes support children's early learning and development, providing them opportunities to engage in activities that build their foundational language, literacy and numeracy skills. This strong foundation can positively impact children's academic success throughout their schooling and beyond [6].

In addition to educational benefits, quality preschool education and care can also have significant social-emotional benefits for children. Preschool programmes allow children to interact with peers, learn social skills and develop positive relationships with adults. This social interaction can help children to develop empathy, communication skills and a sense of belonging, which are crucial for success in school and life [7].

Finally, quality preschool education and care can also benefit children emotionally. According to Bierman et al. [8], preschool programmes provide a safe and supportive environment where children can explore their emotions, develop self-regulation skills, and build resilience. This emotional support can help children manage stress, cope with difficult situations and build self-esteem.

*Perspectives on Preschool Education and Care DOI: http://dx.doi.org/10.5772/intechopen.111745*

Providing quality preschool education and care is crucial to a child's future. It supports children's holistic development, laying the foundation for future academic, social and emotional success. By providing children with the tools, they need to succeed in school and beyond, quality preschool education and care can help to close the achievement gap and promote a brighter future for all children [9].


**4. Conclusions**

Five accessions of *Dendrobium* from Liwa Botanical Garden were identification based on morphological characters and phenetic relationships. The result of analysist 11 morphological characters showed leaf of *Dendrobium* have high variations. The phenetic relationship showed five accessions of *Dendrobium* from Liwa Botanical Garden can be classified into 2 main groups formed with a similarity index value of 0.813. The morphological characters that have a large influence on grouping are the ratio of length and width, cross section, and sitting of leaf based on PCA values. Variability of *Dendrobium* leaf characters can be possible due to the hybridization and outcrossing processes. The resulting phenetic dendrogram topology is supported by the morphological character classification. The results of the observation of 9 anatomical characters on the upper and lower surfaces of the leaves indicate that the leaf organs have high variations. Accessions IR015, CAT 140, and CAT 274 have stomata only on the lower surface, while CAT 144 has stomata on the upper and lower surfaces. This difference is due to the position of the leaves attached to the stem at CAT 144 forming an angle of 45̊C, while the others open horizontally. IR015, CAT 140, and CAT 274 the upper surface of the leaves is only composed of epidermis which is mostly irregular and pentagonal in shape. The highest number was in CAT 274 because the epidermis was smaller than IR015 and CAT 144. The types of stomata in all types were the same, namely tetracytic in the form of stomata surrounded by 4 neighboring cells. The stomata are kidney-shaped and the epidermis is irregular, pentagonal, and hexagonal in shape.


2. OFDM principles

This section gives a brief introduction on the principles of OFDM in radio frequency communication which serves as a basis for further reading. The baseband diagram of OFDM is shown in Figure 1. At the transmitter side, coded information bits are first mapped to symbols through digital modulation such as pulse amplitude modulation (PAM), quadrature amplitude modulation (QAM), and phase shift keying (PSK). Typically, complex-valued QAM modulation is used

OFDM Systems for Optical Communication with Intensity Modulation and Direct Detection http://dx.doi.org/10.5772/intechopen.68199 87

Figure 1. The "IFFT" module at the receiver side should be "FFT" module.

In IM/DD channel, there are still some non-ideal factors that may deteriorate the quality of communication. One key factor is the multipath effect. This effect is caused by several mechanisms. First, in wireless communications, the light could be reflected at multiple locations and by many times by the surroundings before arriving at the receiver side. Second, the modulation bandwidth of LED is limited, typically below 100 MHz. When the bandwidth of signal exceeds the modulation bandwidth of LED, multipath effect occurs. Third, in fiber communication, light components of different wavelength propagate through different paths, which also cause multipath effect. Therefore, effective means of mitigating the multipath effect are

In RF communication, orthogonal frequency division multiplexing (OFDM) is a powerful multi-carrier modulation scheme to combat the multipath effect. Compared to the singlecarrier modulation schemes, OFDM avoids the usage of a complicated high-order timedomain equalizer. Instead, it employs frequency domain equalizer that only has a single tap. This greatly simplifies the equalization task and can perfectly resolves the multipath effects without any residual errors at high signal-to-noise ratio (SNR) region. Thus, introducing OFDM to IM/DD optical communication is a natural choice. However, different from RF communication, IM/DD requires that the transmitted signal must be real and positive, which imposes strict constraint on the modulation scheme and the original OFDM transceiver must be modified carefully to satisfy the new scenario. In addition, different applications may have diverse emphasis such as spectral efficiency, power efficiency, detection capability, as well as

Within such perspectives, the purpose of this chapter was to analyze the potential forms of OFDM that are suitable for IM/DD transmission as well as various receiver designs in optical communication. We first study the concepts and basic modulation schemes of OFDM systems in IM/DD optical communication. They can be generally classified into three categories: directcurrent-biased optical OFDM (DCO-OFDM), non-DC-biased optical OFDM, and hybrid optical OFDM. We will elaborate the system models and explain the validity of some fancy designs in those systems through analysis. Second, we investigate the preliminary receivers of those OFDM systems. Besides, we will propose a new receiver that is capable of improving the detection performance based on the inherent signal structures of the specific transmitted signal. Third, the spectral efficiencies and computational complexities of different systems and receivers are analyzed and compared. Finally, the bit error rate (BER) performance of different systems is compared through computer simulations to give the reader a whole

picture of different candidate OFDM systems in IM/DD optical communication.

This section gives a brief introduction on the principles of OFDM in radio frequency communication which serves as a basis for further reading. The baseband diagram of OFDM is shown in Figure 1. At the transmitter side, coded information bits are first mapped to symbols through digital modulation such as pulse amplitude modulation (PAM), quadrature amplitude modulation (QAM), and phase shift keying (PSK). Typically, complex-valued QAM modulation is used

necessary in IM/DD optical communications.

86 Optical Fiber and Wireless Communications

computational complexity.

2. OFDM principles

in OFDM. Then, the modulated symbols are divided into multiple groups and each group consists of N-modulated symbols, defined as X ¼ ½Xð0Þ,Xð1Þ,…,XðN � 1Þ�T, where the group index is omitted here for simplicity. In OFDM, each modulated symbol XðkÞ is loaded on a subcarrier with center frequency 2π N k and there are N subcarriers in total. All the symbols are transmitted on their subcarriers simultaneously. Mathematically, this is equivalent to transform the vector X by an N-point inverse fast Fourier transform (IFFT) module, resulting in a new vector x ¼ ½xð0Þ,xð1Þ,…,xðN � 1Þ�T, that is,

$$\mathbf{x}(n) = \frac{1}{\sqrt{N}} \sum\_{k=0}^{N-1} \mathbf{X}(k) e^{\frac{2\pi k n}{N}}.\tag{1}$$

In OFDM, X is generally considered as frequency domain signal and x is viewed as time-domain signal. In addition, x is typically called an OFDM symbol, which is different with the modulated symbol aforementioned. Finally, x is appended at its head with a cyclic prefix (CP), which is just the copy of the last few samples of x. In general, the length of CP is no smaller than the length of transmission channel to avoid inter-symbol interference (ISI) between adjacent OFDM symbols.

Assuming the impulse response of the multipath channel is denoted by h ¼ ½hð0Þ, hð1Þ,…, hðL � 1Þ�T ; then, the received signal at the receiver after channel transmission is given by

$$r(n) = h(n) \* \mathbb{x}\_{\varepsilon}(n) + \varepsilon(n),\tag{2}$$

where xcðnÞ is the CP-appended version of the time-domain transmitted signal, zðnÞ is the additive white Gaussian noise (AWGN) with zero mean, and \* denotes linear convolution. The receiver first removes the CP parts of received signal, which results in a new vector y of length N, which can be rewritten as

$$\mathbf{y}(n) = h(n) \otimes \mathbf{x}(n) + \mathbf{z}(n),\tag{3}$$

where ⊗ denotes cyclic convolution. We can see that due to the insertion and removal of CP, the linear convolution is now transformed to a cyclic one, which would be beneficial for equalization, as will be shown in the following text.

From signal processing theory, cyclic convolution in time domain is equivalent to product in frequency domain. Based on this fact, by defining YðkÞ, HðkÞ, and ZðkÞ as the N-point fast Fourier transform of yðnÞ, hðnÞ, and zðnÞ, respectively, one has

$$Y(k) = H(k)X(k) + Z(k), \\ k = 0, 1, \ldots, N - 1. \tag{4}$$

As we can see, each frequency-domain symbol XðkÞ is transmitted as if in a flat channel of response HðkÞ and different symbols transmit in different subchannels (subcarriers) without interfering with each other. This greatly simplifies the equalization task. For example, both zero forcing (ZF) and minimum mean square error (MMSE) equalization can be performed to recover XðkÞ which only involves single-tap equalizer per subcarrier:

$$\widehat{X}(k) = \begin{cases} \frac{Y(k)}{H(k)} & \text{' } \quad \text{ZF} \\\\ \frac{H^\*(k)Y(k)}{\left|H(k)\right|^2 + \sigma\_n^{-2}}, & \text{MMSE} \end{cases} \tag{5}$$

where σn 2 is the variance of noise. The processing in Eqs. (4) and (5) can be realized by performing FFT and per-subcarrier equalization, as shown in Figure 1.

#### 3. Optical OFDM systems for IM/DD channel

#### 3.1. Preliminaries

In IM/DD channel, there is a key difference with RF channel: the transmitted signal must be real and positive. This results from the fact that the intensity of light must be a real and positive quantity. Therefore, the structure for OFDM shown in Figure 1 cannot be directly used in IM/ DD optical channel. Necessary changes must be made instead. A common approach is to generate a real time-domain signal first. This can be realized by imposing Hermitian symmetry on the frequency domain signal X, which is defined as follows:

$$X(N-k) = X^\*(k), \\ k = 1, \ldots, N-1, \\ X(0) = X(N/2) = 0. \tag{6}$$

It can be easily shown that the IFFT of X having property Eq. (6) is a pure real-valued signal x. Based on this real signal, one can further generate a positive signal to drive the optical source by various means. Those resultant new OFDM systems are typically referred to as optical OFDM systems.

#### 3.2. DC-biased optical OFDM

The most straightforward approach to generate a positive signal from a real signal is to impose a proper DC bias. In optical communication, the DC bias is typically chosen such that the mean value of the positive signal just lies on the center point of the linear range of the optical source. This system is called direct current-biased optical OFDM, or DCO-OFDM, whose transmitter is shown in Figure 2.

The clipping module shown in Figure 2 is necessary. Since xðnÞ is Gaussian distributed, it is possible that xðnÞ plus a DC bias is still out of the linear range of the optical source. For example, if an LED accepts driving current within the range of [a, b], where 0 ≤ a < b, then the OFDM Systems for Optical Communication with Intensity Modulation and Direct Detection http://dx.doi.org/10.5772/intechopen.68199 89

Figure 2. Diagram of DCO-OFDM transmitter.

clipping is needed to confine xðnÞ plus a DC bias into this range. Otherwise, the LED could not be illumined due to under-driving or even be damaged due to over-driving.

#### 3.3. Non-DC-biased optical OFDM

Besides DCO-OFDM, there are many forms of optical OFDM systems that are not relying on DC bias. The most famous ones are introduced in this subsection.

#### 3.3.1. ACO-OFDM

YðkÞ ¼ HðkÞXðkÞ þ ZðkÞ, k ¼ 0, 1, …, N � 1: ð4Þ

ðkÞ, k ¼ 1, …, N � 1, Xð0Þ ¼ XðN=2Þ ¼ 0: ð6Þ

ð5Þ

As we can see, each frequency-domain symbol XðkÞ is transmitted as if in a flat channel of response HðkÞ and different symbols transmit in different subchannels (subcarriers) without interfering with each other. This greatly simplifies the equalization task. For example, both zero forcing (ZF) and minimum mean square error (MMSE) equalization can be performed to

YðkÞ

ðkÞYðkÞ

In IM/DD channel, there is a key difference with RF channel: the transmitted signal must be real and positive. This results from the fact that the intensity of light must be a real and positive quantity. Therefore, the structure for OFDM shown in Figure 1 cannot be directly used in IM/ DD optical channel. Necessary changes must be made instead. A common approach is to generate a real time-domain signal first. This can be realized by imposing Hermitian symmetry

It can be easily shown that the IFFT of X having property Eq. (6) is a pure real-valued signal x. Based on this real signal, one can further generate a positive signal to drive the optical source by various means. Those resultant new OFDM systems are typically referred to as optical

The most straightforward approach to generate a positive signal from a real signal is to impose a proper DC bias. In optical communication, the DC bias is typically chosen such that the mean value of the positive signal just lies on the center point of the linear range of the optical source. This system is called direct current-biased optical OFDM, or DCO-OFDM, whose transmitter is

The clipping module shown in Figure 2 is necessary. Since xðnÞ is Gaussian distributed, it is possible that xðnÞ plus a DC bias is still out of the linear range of the optical source. For example, if an LED accepts driving current within the range of [a, b], where 0 ≤ a < b, then the

H�

HðkÞ , ZF

jHðkÞj2 þ σn2 , MMSE

2 is the variance of noise. The processing in Eqs. (4) and (5) can be realized by

recover XðkÞ which only involves single-tap equalizer per subcarrier:

8 >>><

>>>:

performing FFT and per-subcarrier equalization, as shown in Figure 1.

X \_ ðkÞ ¼

3. Optical OFDM systems for IM/DD channel

on the frequency domain signal X, which is defined as follows:

XðN � kÞ ¼ X�

where σn

3.1. Preliminaries

88 Optical Fiber and Wireless Communications

OFDM systems.

shown in Figure 2.

3.2. DC-biased optical OFDM

Asymmetrically clipped optical OFDM (ACO-OFDM) is the most famous non-DC-biased optical OFDM system and has been extensively studied in literature [1]. The basic idea of ACO-OFDM is to generate an asymmetrically structured time-domain signal such that direct clipping at zero (without adding DC bias) is allowed without any information loss. To do so, the frequency-domain input symbol X has a special structure besides satisfying Hermitian symmetry. Specifically, the odd components of X contain useful information U but the even components of X are set to zeros. This is shown in Figure 3.

After IFFT, the time-domain signal x has an asymmetrical structure:

$$\mathbf{x}(n) = -\mathbf{x}\left(n + \frac{N}{2}\right), n = 0, 1, \dots, N/2. \tag{7}$$

As shown in Figure 4, signal x can be directly clipped at zero without adding any DC bias, yet the information is kept after clipping thanks to the asymmetrical structure.

Figure 3. Diagram of ACO-OFDM transmitter.

Figure 4. Asymmetrical structure before and after clipping at zero in ACO-OFDM.

#### 3.3.2. PAM-DMT

Pulse amplitude modulation-discrete multi-tone (PAM-DMT) is another non-DC-biased optical OFDM system [2]. It is similar to ACO-OFDM, in that direct clipping is used. However, the difference is that in PAM-DMT, only the imaginary part of subcarrier input X carries useful information U while the real part is set to zero, as shown in Figure 5. Note that PAM modulation should be used in PAM-DMT rather than QAM in DCO-OFDM and ACO-OFDM.

It can be easily shown that the resultant time-domain signal x also has an asymmetric structure but is slightly different with that of ACO-OFDM, which is shown in Eq. (8) and Figure 6:

$$\mathbf{x}(n) = -\mathbf{x}(N-n), n = 1, 2, \dots, \frac{N}{2}, \mathbf{x}(0) = \mathbf{x}\left(\frac{N}{2}\right) = 0. \tag{8}$$

Figure 5. Diagram of PAM-DMT transmitter.

Figure 6. Asymmetrical structure before and after clipping at zero in PAM-DMT.

#### 3.3.3. Flip-OFDM

3.3.2. PAM-DMT

90 Optical Fiber and Wireless Communications

Figure 5. Diagram of PAM-DMT transmitter.

Pulse amplitude modulation-discrete multi-tone (PAM-DMT) is another non-DC-biased optical OFDM system [2]. It is similar to ACO-OFDM, in that direct clipping is used. However, the difference is that in PAM-DMT, only the imaginary part of subcarrier input X carries useful information U while the real part is set to zero, as shown in Figure 5. Note that PAM modulation should be used in PAM-DMT rather than QAM in DCO-OFDM and ACO-OFDM. It can be easily shown that the resultant time-domain signal x also has an asymmetric structure but is slightly different with that of ACO-OFDM, which is shown in Eq. (8) and Figure 6:

�me

(a) unclipped signal (b) clipped signal

N/2 N-1

Figure 6. Asymmetrical structure before and after clipping at zero in PAM-DMT.

amplitude amplitude

�me

N

2 , xð0Þ ¼ x

N 2

(b) clipped signal

N/2 N-1

¼ 0: ð8Þ

�me

N/2 N-1

�me

xðn޼�xðN � nÞ, n ¼ 1, 2,…,

(a) unclipped signal

Figure 4. Asymmetrical structure before and after clipping at zero in ACO-OFDM.

N/2 N-1

amplitude amplitude

Both ACO-OFDM and PAM-DMT rely on specially designed signal structures on the frequencyand time-domain signals. In contrast, flip-OFDM employs a simpler way such that a general frequency-domain signal X without any fancy structure is accepted [3]. Instead, the real timedomain signal x, without any symmetry, is split into two parts: the first part only contains the samples of positive ones in x, the negative ones are set to zeros; the second part only contains the samples of negative ones, but with flipped signs, and leaves the positive ones as zeros. This is shown in Figure 7.

Mathematically, the first and second parts of the flipped signal are given by

$$\mathbf{x}\_1(n) = \frac{\mathbf{x}(n) + |\mathbf{x}(n)|}{2}, \mathbf{x}\_2(n) = \frac{-\mathbf{x}(n) + |\mathbf{x}(n)|}{2}, n = 0, 1, \dots, N - 1. \tag{9}$$

After flip processing, the two signal parts are appended with CP, respectively, and are transmitted on channel consecutively. In some literature, flip-OFDM is also referred to as unipolar OFDM (U-OFDM).

Figure 7. Signal structure before and after flipping processing in flip-OFDM.

#### 3.4. Duality of non-DC-biased optical OFDM systems

This section gives a brief introduction on the duality of the non-DC-biased optical OFDM systems. Based on this duality, many receiver design methods could be easily extended from one system to other systems.

For ACO-OFDM, the transmitted signal is given by

$$\mathbf{x}\_c = (\mathbf{x} + |\mathbf{x}|)/2,\tag{10}$$

and x can be written as x ¼ ½x1; � x1� T, where x1 is the first half of x. Therefore, the first and second halves of xc can be written as

$$\mathbf{x}\_{c,1}(n) = \frac{\mathbf{x}\_1(n) + |\mathbf{x}\_1(n)|}{2}, \mathbf{x}\_{c,2}(n) = \frac{-\mathbf{x}\_1(n) + |\mathbf{x}\_1(n)|}{2}, \tag{11}$$

which is exactly the same as the model in Eq. (9) except that the size is changed from N to N/2. For PAM-DMT, the transmitted signal is also given by Eq. (10). However, the unclipped signal x is slightly different, that is, x ¼ ½x1;x2� T, where x2 ¼ �Jx1 with J being a matrix whose anti-diagonal elements are 1s and other elements are all 0s. Now, the first and second halves of the transmitted signal are given by

$$\mathbf{x}\_{c,1} = \frac{\mathbf{x}\_1 + |\mathbf{x}\_1|}{2}, \mathbf{x}\_{c,2} = \frac{-f\mathbf{x}\_1 + f|\mathbf{x}\_1|}{2}. \tag{12}$$

However, JJ = I; therefore, by defining xc,3 ¼ Jxc,2, we have

$$\mathbf{x}\_{c,1} = \frac{\mathbf{x}\_1 + |\mathbf{x}\_1|}{2}, \mathbf{x}\_{c,3} = \frac{-\mathbf{x}\_1 + |\mathbf{x}\_1|}{2}. \tag{13}$$

Now, Eq. (13) is exactly the same as Eqs. (9) and (11).

Therefore, we can see that ACO-OFDM, PAM-DMT, and flip-OFDM essentially share the same signal structure and there is a duality between them. Based on this fact, the receivers designed for one system can be readily extended to other systems with simple substitution of variables.

#### 3.5. Hybrid systems

Beside the basic forms of DC and non-DC-biased optical OFDM systems, there also exist some hybrid ones where multiple basic systems are superimposed in a specially designed fashion. In general, hybrid systems can be further classified into three categories.

#### 3.5.1. Hybrid optical OFDM based on DCO-OFDM and a non-DC-biased one

A representative for this kind of system is ADO-OFDM, which combines DCO-OFDM and ACO-OFDM in a special way [4]. Specifically, in ACO-OFDM, the useful data are only loaded on the odd subcarriers, as illustrated in Figure 3, the even subcarriers are forced to be zero. After clipping in time domain, the clipping noise only falls onto even subcarriers and the odd subcarriers are not affected by the clipping noise. At the receiver side, the data could be recovered by using only the odd subcarriers. With the recovered data, one can further perfectly reconstruct the clipping noise on even subcarriers. Therefore, in ACO-OFDM, the even subcarriers can be exploited to load more data, which is the basic idea of ADO-OFDM.

In ADO-OFDM, the odd subcarriers are performed exactly the same as the ACO-OFDM. For the even subcarriers, a modified DCO-OFDM signal is generated, in which only the even subcarriers are used. Then, the signals generated from ACO-OFDM and DCO-OFDM are added together to obtain the ADO-OFDM signal. At the receiver side, ACO-OFDM signal, which is on odd subcarriers, are first detected. Then, the clipping noise on even subcarriers is estimated and subtracted. After that, the even subcarriers contain only DCO-OFDM signal, which is finally decoded.

#### 3.5.2. Hybrid optical OFDM based on two different non-DC-biased ones

HACO-OFDM, or hybrid ACO-OFDM, combines ACO-OFDM and PAM-DMT in one system [5]. The basic idea is similar to that of ADO-OFDM, that is, the odd subcarriers are used for ACO-OFDM transmission while the even subcarriers are used for PAM-DMT transmission. At the receiver side, interference cancellation is used for even subcarriers before decoding PAM-DMT signal. An alternative form for HACO-OFDM is also proposed [6].

#### 3.5.3. Hybrid optical OFDM based on a same non-DC-biased one

anti-diagonal elements are 1s and other elements are all 0s. Now, the first and second halves of

2 , xc,2 ¼ �Jx1 þ Jjx1j

2 , xc,3 ¼ �x1 þ jx1j

Therefore, we can see that ACO-OFDM, PAM-DMT, and flip-OFDM essentially share the same signal structure and there is a duality between them. Based on this fact, the receivers designed for one system can be readily extended to other systems with simple substitution of variables.

Beside the basic forms of DC and non-DC-biased optical OFDM systems, there also exist some hybrid ones where multiple basic systems are superimposed in a specially designed fashion. In

A representative for this kind of system is ADO-OFDM, which combines DCO-OFDM and ACO-OFDM in a special way [4]. Specifically, in ACO-OFDM, the useful data are only loaded on the odd subcarriers, as illustrated in Figure 3, the even subcarriers are forced to be zero. After clipping in time domain, the clipping noise only falls onto even subcarriers and the odd subcarriers are not affected by the clipping noise. At the receiver side, the data could be recovered by using only the odd subcarriers. With the recovered data, one can further perfectly reconstruct the clipping noise on even subcarriers. Therefore, in ACO-OFDM, the even subcarriers can be exploited to load more data, which is the basic idea of ADO-OFDM.

In ADO-OFDM, the odd subcarriers are performed exactly the same as the ACO-OFDM. For the even subcarriers, a modified DCO-OFDM signal is generated, in which only the even subcarriers are used. Then, the signals generated from ACO-OFDM and DCO-OFDM are added together to obtain the ADO-OFDM signal. At the receiver side, ACO-OFDM signal, which is on odd subcarriers, are first detected. Then, the clipping noise on even subcarriers is estimated and subtracted. After that, the even subcarriers contain only DCO-OFDM signal,

HACO-OFDM, or hybrid ACO-OFDM, combines ACO-OFDM and PAM-DMT in one system [5]. The basic idea is similar to that of ADO-OFDM, that is, the odd subcarriers are used for ACO-OFDM transmission while the even subcarriers are used for PAM-DMT transmission.

2 : ð12Þ

2 : ð13Þ

xc,1 ¼ x1 þ jx1j

xc,1 ¼ x1 þ jx1j

general, hybrid systems can be further classified into three categories.

3.5.2. Hybrid optical OFDM based on two different non-DC-biased ones

3.5.1. Hybrid optical OFDM based on DCO-OFDM and a non-DC-biased one

However, JJ = I; therefore, by defining xc,3 ¼ Jxc,2, we have

Now, Eq. (13) is exactly the same as Eqs. (9) and (11).

the transmitted signal are given by

92 Optical Fiber and Wireless Communications

3.5. Hybrid systems

which is finally decoded.

Another form of hybrid optical OFDM is to superimpose multiple blocks of signals from a same non-DC-biased OFDM system. For example, enhanced unipolar OFDM (eU-OFDM) involves multiple blocks of signals from flip-OFDM [7]. Figure 8 shows its time-domain structure with three layers [8], where the symbols xþ i,j and x� i,j denote, respectively, the positive and flipped negative parts of the original j-th bipolar signal xi,j from layer-i. Each layer is just a repetition of flip-OFDM time-domain signal. We can see that for the first layer, four normal flip-OFDM symbols are used. For the second layer, two normal flip-OFDM symbols are repeated two times. For the third layer, one normal flip-OFDM symbol is repeated four times. Then, all the time symbols from three layers are added for transmission.

The receiver detection is very simple. The first layer is firstly decoded using normal subtraction. The second and third layers do not interfere in this procedure due to perfect selfcancellation. After the first layer is decoded, its impact is subtracted from the received signal. Then, the second layer is decoded subsequently. Then, the second layer signal is subtracted from the received signal and the third layer is decoded finally.

Besides eU-OFDM, the overlapping of ACO-OFDM or PAM-DMT is also proposed in literatures [9–11]. They all share similar idea with eU-OFDM and the receiver is based on layer-bylayer decoding.

Figure 8. Illustration of a three-layer eU-OFDM time-domain signal components.