Amira Methni

Belgacem Matthieu Lemerre

Belgacem Ben Hedia

Serge Haddad
email: haddad@lsv.ens-cachan.fr

Kamel Barkaoui
email: kamel.barkaoui@cnam.fr

Verifying and Constructing Abstract TLA Specifications: Application to the Verification of C programs

Keywords: Anything, Something, Everything else

come   L'archive ouverte pluridisciplinaire

I. INTRODUCTION

As software systems become large and error-prone, formal verification methods become an essential key concept to ensure their correctness. Model Checking [START_REF] Clarke | Model checking[END_REF] provides an automated technique to check and detect errors in computer programs. But despite its promise, the verification process may be complex due to the size of these systems. One useful technique to reduce the complexity of verification process is abstraction. Generally, an abstract model specify "what" the system do while the concrete model describes "how". The idea is to map the concrete set of states to a smaller set of states resulting in an approximation of the system with respect to the property of interest. We say that the concrete model implements the abstract one. Verifying the abstract model is generally more efficient than verifying properties of the original.

a) Contributions: We define an operational semantics of a TLA+ specification in terms of automata, that we called "state transition system" (STS). We remind the concepts of implementation relation and refinement mapping in TLA+ that we formalize in terms of relations between STSs. The refinement between specifications can be checked with the TLC model checker. Verified properties on the abstract specification can thus be deduced in the concrete specification. A way to abstract details of the concrete specification is to hide its irrelevant variables. TLA+ can express data hiding, but TLC can't support this type of construct. So, we have implemented the notion of data hiding by constructing a STS that we call "quotient STS", which is constructed by extending the TLC model checker. In order to let the quotient STS be analyzed by existing tools, we extend the TLC model checker to produce an LTS that can be checked by the CADP toolkit. We apply the mentioned concepts on C programs using our tool C2TLA+. Preliminary results shows the importance of using an abstract model to reduce the complexity of verification. b) Outline: The remainder of the paper is structured as follows. We give an overview of TLA+ and its operational semantics in Section 2. Section 3 reminds the concepts of refinement mapping and the implementation relation between specifications and describe a way to construct the quotient STS. In Section 4, we apply these concepts to verify the correctness of the C implementation with respect to their specification and we report some preliminary experimental results obtained. We discuss related work in Section 5. Section 6 concludes and presents future research directions.

II. AN OPERATIONAL SEMANTICS FOR TLA

SPECIFICATION

In this section, we explain some basics concerning the syntax and the semantics of TLA [START_REF] Lamport | Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers[END_REF]. Then, we describe the operational semantics of TLA using a State Transition System.

A. Overview of TLA+

TLA+ is a formal specification language based on the Temporal Logic of Actions (TLA) [START_REF] Leslie | The Temporal Logic of Actions[END_REF] for the description of reactive and distributed systems. TLA itself is a variant of linear-time temporal logic. The semantics of TLA is defined in terms of states. A state is a mapping from variables to values. A state function is a nonboolean expression built from constants, variables and constant operators, that maps each state to a value. For example, y + 3 is a state function from a state s to three plus the value that s assigns to the variable y. An action is a boolean expression containing constants, variables and primed variables (adorned with " " operator). Unprimed variables refer to variable values in the actual state and primed variables refer to their values in the next-state. Thus, an action represents a relation between old states and new states. For example, x = y + 2 is an action asserting that the value of x in the old state is two greater that the value of y in the new state. A state predicate (or predicate for short) is an action with no primed variables.

Syntactically, TLA formulas are built up from actions and predicates using boolean operators (¬ and ∧ and others that can be derived from these two), quantification over logical variables (∀, ∃), the operators and the unary temporal operator (always) of linear temporal logic [START_REF] Manna | The Temporal Logic of Reactive and Concurrent Systems[END_REF].

The expression [A]

vars where A is an action and vars the tuple of all system variables, is defined as A ∨ (vars = vars). It states that either A holds between the current and the next state or the values of vars remain unchanged when passing to the next state. For any action A, the state predicate Enabled (A) describes whether the action A can be executed in the current state s, i.e., there exists some state t such that s -→ t is an A step.

To specify a system in TLA, one describes its allowed behaviors. A behavior is an infinite sequence of states that represents a conceivable execution of the system. The system specification can be given by the temporal formula Φ defined as a conjunction of the form:

Φ ∆ = Init ∧ [Next] vars ∧ F (1)
where, Init is the predicate describing all legal initial states, Next is the next-state action defining all possible transitions between states and F is a conjunction of fairness assumptions about the execution of actions. However, other forms of specification are possible and can occasionally be useful.

A TLA formula is true or false on a behavior, which is a sequence of states. Let σ = s 0 , s 1 , . . . be a behavior. σ satisfies Spec iff Init is true of the first state s 0 and every state that satisfies Next or a "stuttering step" that leaves all variables unchanged.

B. State Transition System

In TLA, the behavior of a system is modeled as an infinite sequence of states. The operational semantics of a TLA specification can be given in terms of a State Transition System (STS), which is easier to work with than sets of sequences. Figure 1 shows a TLA specification and its corresponding STS T Φ = (Q Φ , I Φ , δ Φ ) which encodes all its possible behaviors (÷ symbol denotes integer division). The specification Φ is translated into T Φ as follows:

Φ ∆ = (x = 0 ∧ y = 0) ∧ [ ∧ x = (x + 1)%4 ∧ y = x ÷ 2 ] x ,y (
-T Φ has initial state(s) I Φ specified by the predicate x = 0 ∧ y = 0, -every state s ∈ Q Φ corresponds to a valuation of the state function x , y , -each transition t ∈ δ Φ corresponds to satisfying the predicate [x = (x + 1)%4 ∧ y = x ÷ 2] x ,y .

III. REFINEMENT AND ABSTRACTION OF TLA SPECIFICATIONS A way to reduce the verification task is to define an abstract model as a specification, and then relate behaviors of the abstract model to those of the implementation. Properties checked on the abstract model can be deduced on the concrete one. We use concrete model to refer to high-level specification and abstract model to refer to low-level specification. This section describes the semantics of refinement between a high-level and a low-level TLA+ specifications. Then, we present a way to automatically construct a reduced model, which abstracts the detailed behavior of the concrete TLA+ specification.

A. Refinement Mapping

Abadi and Lamport [START_REF] Abadi | The Existence of Refinement Mappings[END_REF] described that a high-level specification Ψ implements a low-level specification Φ iff for each behavior of Ψ, there is a behavior of Φ with the same sequence of externally visible states, allowing stuttering, e .g., if the state Φ does not change during a finite number of steps. This implementation relation is proved by defining a refinement mapping between specifications.

Let Ψ and Φ be two TLA specifications, x 1 , . . . , x m and y 1 , . . . , y n the variables occurring in the specifications Ψ and Φ respectively. A (concrete) specification Ψ implements an abstract specification Φ if Ψ ⇒ Φ. The proof of this implication consists in defining state functions ȳ1 , . . . , ȳn in terms of the variables y 1 , . . . , y n and prove that Ψ ⇒ Φ, where Φ denote the formula Φ obtained by substituting ȳi for the free occurrences of y i , for all i .

The set of state functions ȳ1 , . . . , ȳn is called a refinement mapping. The "barred variable" ȳi is the state function with which Ψ implements the variable y i of Φ. So, if σ is the behavior s 1 → s 2 → s 3 . . . of Ψ, we define the behavior σ to be s1 → s2 → s3 . . . We say that Ψ implements Φ under this refinement mapping iff, for each behavior σ satisfying Ψ, the behavior σ is a behavior of Φ.

B. Implementation Relation and Property Preservation

The proof Ψ ⇒ Φ under a refinement mapping is sufficient to verify that Ψ implements Φ [START_REF] Abadi | The Existence of Refinement Mappings[END_REF]. The key to the implication relation is that TLA allows to write only formula that are insensitive to stuttering, i.e., given a TLA formula Φ and two stuttering equivalent runs σ and σ , Φ holds along σ if and only if it holds along σ [START_REF] Leslie | The Temporal Logic of Actions[END_REF]. This implementation relation between TLA specifications can be viewed as a weak simulation relation between its corresponding STSs.

Definition 2:

Let T Ψ = (Q Ψ , I Ψ , δ Ψ ) and T Φ = (Q Φ , I Φ , δ Φ ) denote two STSs. A simulation R relation from Q Ψ to Q Φ is
a function that satisfies the following conditions: If a lower-level specification, expressed by a TLA formula Ψ, implements an abstract specification Φ, Ψ preserves all TLA properties of Φ if and only if for every formula φ, if Φ ⇒ φ is valid, then so is Ψ ⇒ φ. This is true if Ψ ⇒ Φ.

• ∀s ∈ I Ψ , R(s) ⊆ I Φ (initial

C. Data Hiding in TLA

A very useful form of data abstraction is variable hiding, which refers to providing only essential information to the outside world and hiding not needed information. In TLA, it is possible to hide some variables using the existential quantifier ∃ ∃ ∃ ∃ ∃ ∃ (which differs from the quantifier of predicate logic). The formula ∃ ∃ ∃ ∃ ∃ ∃ x : Φ asserts that it doesn't matter what the actual values of x are, but that there are some values x can assume for which Φ holds. The meaning of ∃ ∃ ∃ ∃ ∃ ∃ is defined by formula 2. The formula σ ∼ x is defined to be true iff σ can be obtained from τ (or vice-versa) by adding and/or removing stuttering steps and changing the values of x . Thus, the formula 2 is true for a behavior σ iff Φ is true for some behavior τ such that σ ∼ x τ is true.

σ |= ∃ ∃ ∃ ∃ ∃ ∃ x : Φ ∆ = ∃ behavior (σ ∼ x τ ) ∧ (τ |= Φ) (2)
The temporal formula (3) describes a specification Φ where v is the list of all relevant state variables and x is the list of internal (hidden) variables.

Φ ∆ = ∃ ∃ ∃ ∃ ∃ ∃ x : Init ∧ [Next] v ∧ L (3)
The existential operator is a very simple and useful way in which the system is described as a black box. However, in practice, the TLC model checker cannot handle the TLA hiding operator. In what follows, we present a way to implement data hiding by construct a quotient STS from a TLA specification. Given a concrete STS T = (Q, I, δ) describing a TLA specification, one can obtain an abstraction of T , a small STS that we call quotient STS and which is obtained by quotienting the states Q under a refinement mapping γ.

D. Computing a Quotient STS

Figure 2 shows a STS resulting from adding a refinement mapping ȳ ∆ = y in all states of the concrete STS. The quotient STS (at the right side of the figure) is constructed by collapsing all states related under the relation γ into the same state. Let T / γ = (Q/ γ , I/ γ , δ/ γ ) be the quotient state transition system of T = (Q, I, δ) under the refinement mapping γ. The algorithm of constructing T / γ is given by the algorithm 1.

We extend the implementation of TLC to produce the quotient STS "on-the fly" when the TLC model checker computes the state space of a specification. In fact, TLC makes efficient use of disk. It doesn't keep all states in memory which is the limiting factor of the explicit other model checkers. Instead, it stores just fingerprints of states, which is a 64-bit number generated by a "hashing" function. So, the probability that two states have the same fingerprint is 2 -64 which is a very small number. So, the quotient STS is generated with the same fingerprint collision probability and without exploding the memory.

Q γ ← γ(I) 3: NotSeen ← {s ∈ Q | s ∈ Q and (s, s ) ∈ δ} 4:
while NotSeen = {} do 5:

for ∀q ∈ NotSeen do 6:

if γ(q) / ∈ Q γ then 7: Q γ ← Q/ γ ∪ {γ(q)} 8:
δ/ γ = δ/ γ ∪ {(γ(q), γ(q )) | (q, q ) ∈ δ} end for 12:

end while 13: end procedure

E. Translating a STS into a Labelled Transition System

In order to use existing tools to check properties on a STS, we transform the quotient STS into a Labelled Transition System (LTS), that we call quotient LTS.

Definition 3: A Labelled Transition System is 4-tuple T = Q, L, δ, s 0 , where:

• Q is the set of states, • L is the set of action labels, • δ is the transition relation (a subset of Q × L × Q),
• and s 0 is the initial state. A transition (s 1 , l , s 2 ) of δ, indicates that the system can move from state s 1 to state s 2 by performing action labelled by l . c) Property preservation.: The equivalence between checking a property given in LTL \x (Linear Temporal Logic without the "next operator") on the quotient LTS and checking it on the original LTS is ensured by the preservation.

Proposition 1: Let ϕ be an LTL \x formula, let T Φ and T Ψ be two STSs such that

T Ψ ⇒ T Φ . If T Φ |= ϕ then T Ψ |= ϕ F.

Usefulness of the Quotient LTS

The quotient LTS abstracts away the details of the concrete specification, its main advantage is its small size. As properties are preserved between the concrete specification and its quotient, model checking properties can be done on the quotient LTS directly, which is a simple task. The quotient LTS is generated once and can be used to verify different properties (modulo the refinement mapping).

To express and check properties on the quotient STS, we use the CADP [START_REF] Garavel | CADP 2011: a toolbox for the construction and analysis of distributed processes[END_REF] toolkit. For this, we first adapt the label names such that LTS can be parsed by the CADP tools. Then, we express properties in the MCL (Model Checking Language) [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF] language, the property specification language of CADP that can be verified by its associated model checker. In this section, we implement the concept of refinement between TLA+ specifications and the quotient LTS on C programs. Figure 3 illustrates the verification flow of C programs. We use our tool C2TLA+ [START_REF] Methni | Specifying and Verifying Concurrent C Programs with TLA+[END_REF] to translate C programs into (a concrete) TLA+ specification. This latter can be checked directly against a set of properties, or against an abstract specification by defining the refinement mapping and the implementation relation between the concrete and the abstract specifications. Properties can be expressed in TLA to be verified using the TLC model checker. The quotient LTS is generated, and MCL properties can be verified by the CADP model checker.

In what follows, we briefly present how we specify the semantics of C in TLA+. We apply the described notions by considering the example of the dining philosophers. Finally, we assess the usefulness of using abstraction by giving results of properties verification using TLC and the CADP model checker.

A. TLA specification of a C program C2TLA+ [START_REF] Methni | Specifying and Verifying Concurrent C Programs with TLA+[END_REF] generates a TLA specification that describes the behavior of the C program as a closed system according to a set of translation rules. A concurrent program consists in a set of C functions. In C2TLA+, concurrency is modeled by considering all possible interleaving of sequences of operations called processes (corresponding to threads in C). Each step of the complete specification is attributed to exactly one process. The C program is defined by a TLA formula in the form of 1. Fore more detailed information about the translation from C to TLA+, please refer to our previous work [START_REF] Methni | Specifying and Verifying Concurrent C Programs with TLA+[END_REF].

B. Illustrating Example

As an example, we consider the classic dining philosophers problem. One possible solution to this problem is the one that appears in Tanenbaum's popular operating systems textbook [START_REF] Tanenbaum | Modern Operating Systems[END_REF], given in Figure 4.

In the implementation of this solution, the global semaphore mutex provides mutual exclusion for execution of critical sections and the semaphore sem[i] ensures synchronization. The latters perform P() to acquire a lock and V() to release it, using CAS ("Compare-and-swap") primitive. We define a coarsest-grained representation of the dining philosopher, illustrated by Figure 5 that captures the aspects of the system that interest us without giving all the details of its internal structure.

# d e f i n e N 4 # d e f i n e LEFT ( i ) ( i +N-1)%N # d e f i n e RIGHT ( i ) ( i + 1 )%N # d e f i n e THINKING 0 # d e f i n e HUNGRY 1 # d e f i n e EATING 2 t y p e d e f i n t s e m a p h o r e ; i n t s t a t e [N ] ; s e m a p h o r e mutex ; s e m a p h o r e sem [N ] ; v o i d p h i l o s o p h e r ( i n t i )

{ w h i l e (
In order to check liveness properties we consider that the philosopher cannot starve waiting for a fork i.e., no philosophers is eating forever. This assumption is stated by the formula Fairness, where WF vars (A) denotes weak fairness on action A.

Fairness ∆ = ∧ ∀ i ∈ (0 . . N -1) : WFvars (hungry(i)) ∧ WFvars (eat(i)) ∧ ∀ i ∈ (0 . . N -1) : ♦(ENABLED think (i) vars ) =⇒ ( ♦ eat(i) vars )
e) Specifying the refinement relation.: To check that the concrete specification, generated by C2TLA+, implements the abstract version of the dining philosophers, we define the MODULE Abstract philosophers EXTENDS Naturals, TLC CONSTANT N VARIABLES phil state, forks vars ∆ = phil state, forks fork available(i)

∆ = forks[i] = N fork acquire(p, i) ∆ = forks = [forks EXCEPT ! [p] = i] forks release(p) ∆ = forks = [forks EXCEPT ! [p] = N , ! [(p + 1)%N ] = N ] fork release(p) ∆ = forks = [forks EXCEPT ! [p] = N ] LEFT (p) ∆ = (p + 1) RIGHT (i) ∆ = IF (i = 0) THEN (N -1) ELSE (i -1) think (ph) ∆ = ∧ phil state[ph] = "think" ∧ fork available(LEFT (ph)) ∧ fork acquire((LEFT (ph), ph) ∧ phil state = [phil state EXCEPT ! [ph] = "hungry"] hungry(ph) ∆ = ∧ phil state[ph] = "hungry" ∧ IF (fork available(ph)) THEN ∧ fork acquire(ph, ph) ∧ phil state = [phil state EXCEPT ! [ph] = "eat"] ELSE ∧ fork release(LEFT (ph)) ∧ phil state = [phil state EXCEPT ! [ph] = "think"] eat(ph) ∆ = ∧ phil state[ph] = "eat" ∧ forks release(ph) ∧ phil state = [phil state EXCEPT ! [ph] = "think"] Init ∆ = ∧ phil state = [i ∈ (0 . . (N -1)) → "think"] ∧ forks = [i ∈ (0 . . (N -1)) → N ] Spec ∆ = Init ∧ [∃ i ∈ 0 . . (N -1) : think (ph) ∨ hungry(ph) ∨ eat(ph)]vars ∧ Fairness Figure 5
. Abstract TLA+ version of the dining philosophers refinement relation as shown in Figure 6. In this section, we don't illustrate the translation of the C code, as the translation rules are described in our previous work [START_REF] Methni | Specifying and Verifying Concurrent C Programs with TLA+[END_REF].

The implementation relation is an implication formula Spec ⇒ Abstract instance!Spec.

D. Expressing properties

An interesting property that the implementation should hold is that the critical sections are protected with the primitives P() and V(). This property can be simply expressed in TLA+ (on the abstract specification) as follows:

mutual exclusion ∆ = ∀ i ∈ (0 . . (N -1)) : (phil state[i] = "eat") =⇒ (phil state[LEFT (i)] = "eat" ∧ phil state[RIGHT (i)] = "eat")
The dining philosophers problem captures many aspects of liveness. Among liveness properties of the dining philosophers is starvation-freedom and deadlock freedom that we expressed in TLA+ as follows:

E. Verification results and comparison

We check that the concrete TLA+ specification (generated by C2TLA+) implements the abstract TLA+ specification (given in figure 6). We also check the set of properties on these two specifications. We extract the quotient LTS from the concrete specification that we checked against the set of properties that we express in MCL. Table I shows the number of states and the verification time of the concrete and the abstract specifications using TLC, and the numbers of states, transitions and the time verification of the quotient LTS using CADP model checker. For 5 philosophers, the state space of the concrete TLA specification exceeds 113 millions states and its verification takes more than 10 hours to check the properties. For the same number of philosophers, the abstract TLA specification generates 82 states and properties were checked in only 1 minute using TLC. On the other hand, the quotient LTS generated 47 states and its verification time is 42s. Due to the preservation properties, we can deduce that all the verified properties on the abstract TLA specification or on the quotient LTS are verified on the concrete specification. The use of abstraction reduces considerably the complexity of verification of C implementations.

When TLC reports that a transition violates the implementation formula Spec ⇒ Abstract instance!Spec, there is an error either in the concrete specification, the abstract specification, or the refinement mapping function. The trace given by TLC can help to determine which one of those is the case. We use our tool to translate this trace in C and get the C execution sequence that leads to the error.

V. RELATED WORK Predicate abstraction [START_REF] Graf | Construction of Abstract State Graphs with PVS[END_REF] is a technique to abstract a program so that only the information about the given predicates are preserved. This technique is being used in SLAM [START_REF] Ball | The SLAM project: Debugging System Software via Static Analysis[END_REF], BLAST [START_REF] Henzinger | Software Verification with BLAST[END_REF] and MAGIC [START_REF] Chaki | Modular verification of software components in c[END_REF]. Their approach has been shown to be very effective on specific application domains such as device drivers programming. SLAM uses symbolic algorithms, while BLAST is an on the fly reachability analysis tool. The MAGIC tool uses LTS models, and weak simulation as a notion of conformance of a system and its asbtract specification.

These tools are applied to C programs and use automated theorem prover to construct the abstraction of the C program. The difficulty of these refinement based approach is that performing a refinement proofs between an abstract and a refined model require non trivial human effort and expertise in theorem proving to get the prover to discharge the proof obligations. SLAM cannot deal with concurrency, BLAST cannot handle recursion.

Besides predicate abstraction, several verification techniques for C programs have been proposed. CBMC [START_REF] Clarke | A Tool for Checking ANSI-C Programs[END_REF] is a bounded model checker for ANSI C programs which translates a program into a propositional formula (in Static Single Assignment form) which is then fed to a SAT solvers to check its satisfiability. CBMC explores program behavior exhaustively but only up to a given depth.

Compared to previous related works that use an overapproximation of the code implementation which is sound, our approach is based on constructing an executable abstract model, that can be expressed using TLA+ or by constructing the quotient LTS. Moreover, TLA+ is a logic that can express safety and liveness properties unlike SLAM, BLAST and CBMC which have limited support for concurrent properties as they only check safety properties.

VI. CONCLUSION AND FUTURE WORK

We have defined an operational semantics of a TLA+ specification in terms of State Transition Systems. We redefined the semantics of refinement between a high-level (concrete) and a low-level (abstract) TLA+ specifications using STSs and we illustrated a way to automatically construct a quotient STS from the concrete specification by extending the TLC model checker. We applied all these notions for verifying C programs. Experimental results show that verifying properties on the abstract model reduces considerably the complexity of the verification process.

As future work, we plan to extend this work on several interesting directions. We would like to generate TLA+ and MCL properties from the ACSL [START_REF] Baudin | ACSL: ANSI/ISO C Specification Language, version 1.4[END_REF] specification language used in Frama-C. We envisage to benefit from Frama-C analysis of shared variables by several processes to generate TLA+ code with less interleaving between the processes, to reduce the state space. Finally, we aim to use the TLA+ proof system [START_REF] Cousineau | TLA+ Proofs[END_REF] to prove refinement between a concrete and abstract specifications.

Figure 1 .Definition 1 :

 11 Figure 1. The operational semantics of a TLA specification . Definition 1: A State Transition System is a 3-tuple T = (Q, I, δ) given by -a finite set of states Q, -a set I ⊆ Q of initial states, -a transition relation δ ⊆ Q × Q.

Figure 2 .

 2 Figure 2. Constructing the quotient STS using the refinement mapping ȳ ∆ = y

Algorithm 1

 1 Construction of the quotient STS 1: procedure QUOTIENTSTS 2:

Figure 3 .

 3 Figure 3. Verification flow of C programs

Figure 4 .

 4 Figure 4. Tanenbaum's solution for the dining philosophers

  MODULE refinement definition EXTENDS Concrete philosophers philNum ∆ = load ("unused", Addr N ) get val (addr , off ) ∆ = load ("unused", [loc → addr .loc, offs → addr .offs + off ]).val refmap(addr ) ∆ = [i ∈ (0 . . philNum) → LET val ∆ = get val (addr state, i) IN IF val = 0 THEN "think" ELSE IF val = 1 THEN "hungry" ELSE "eat" ] Abstract instance ∆ = INSTANCE Asbtract philosophers WITH N ← philNum, phil state ← refmap(Addr state) Spec =⇒ Abstract instance ! Spec

Figure 6 .

 6 Figure 6. Definition of refinement relation between abstract and concrete TLA+ specifications of the dining philosophers

TABLE I .

 I Runtimes of model checking 1

			Verification using TLC		Verification using CADP
	Philos	Concrete Spec.	Abstract Spec.		Quotient LTS
		States	Time(s) States	Time(s) States	Transitions	Time(s)
	3	395K	157	14	15	14	32	12
	4	27.285K 1.080	32	23	20	100	20
	5	113.285K >36.000 82	64	47	147	42

Experiments were carried on an Intel Core Pentium i7-2760QM with 8 cores (2.40GHz each) machine, with 8Gb of RAM memory


Jean Rouch

Enrico Fulchignoni

Claudine De

Albert Astre

"Les Regards Comparés"and"le Bilan du film ethnographique"Jean Rouch's initiatives

Formation de recherches cinématographiques)which he directed until 1980, when Claudine de France took over the position. In 1976, in collaboration with historian Georges

the Super8mm, it was a real opportunity to free the means of expression. From an economic point of view also, it was challenging the system: 10minutes of 16mm, after being processed cost around 150 euros. In super 8mm, 10mins cost 15 euros. So, when in 1978 he decided to set up a new platform called les Regards Comparés2 , he was concretely offering an open spacewhere students, ethnographers, sociologists, filmmakers, artists and non-specialists audience could share films produced in the same geographical or cultural area but from a very distinctive point of view. He was prolonging the famous declaration of Leroy [START_REF] Gourhan | Cinéma et sciences humaines-Le film ethnologique existe-til ?[END_REF]: "The ethnographical label can apply to research film, scientific recording, public documentary, or films about exoticism. All fall under the name of travel film and milieu films shot without any scientific intention yet imbued with ethnologic value upon exportation..."3 Those categories highlight how the milieu film "unconsciously harbors scientific values most evident in changing the viewer's perspective.»Even if for Sol Worth this classification could be perceived as tautological, because each film could be perceived in different ways depending on the conditions of the screening and the audience, in the case of the Regards Comparés, the appeal and the richness of such event came from the confrontation of different points of view over the course of a three-day event. The viewers were given the opportunity to watch films produced by TV producers,travellers and ethnographers in a time-space continuum. Faye Ginsburg recalled it in these terms:« The events brought together people from all over the world, including anthropologists, filmmakers, television executives,video artists, amateur movie makers, as well as people from the societies being viewed, to begin to see how different media agendas, as well as the culture/nationality and gender of producers, shape the images produced ». 3 (1995) In 1978, the first Regards Comparés was organised under the presidency of ProfessorsGeorges Henry Rivière 4 , Enrico Fulchignoni and Meyer Fortes 5 .Rouch advocatedfor collaborations with friends and throughout his career he built up a tribe of friends, all over the world.The Yanomami was the population selected because important audiovisual archives existed but also because one of his best friends, was Tim Ash, who produced Ax fight, a milestone film reference for all those involved in Visual Anthropology.

For the second Regards Comparés, Rouch decided to invite his friend and colleague John Marshall who was involved for many years with the Bushmen of Kalahari. Rouch admired the films of John Marshall and the topic was alsorelevant in terms of comparison, as many films have been produced about the Bushmen.It was a challenging approach and a peculiar moment, which underlined the implicit rules of the ethnographic film.As students, it was a magisterial class where the demonstration of ideas came naturally from the screen and also the discussions.

The CNRS organised this event in the main cinema hall and researchers from all over the world who were interested in the Bushmen, filled the room. Historically, it was very resonant for a young scholar attending the event to listen to each specialist naming the Bushmen as theirs, "my Bushmen do things this way"…. "Mine are different…". 1978 was a turning point and with the 80s approaching fast, the discussion evolved along with the perception of the ethnographers and filmmakers toward the people with whom they shared their fieldwork.

As Faye Ginsburg explained in one of her aticles,« …Yet, byjuxtaposing these different but related kinds of cinematicperspectives on culture, one can create a kind of parallax effect; if harnessed analytically, these "slightly different angles of vision" can offer a fuller comprehension of the complexity of the social phenomenon we call culture and those media representations that selfconsciously engage with it ». 6 She alsoalso underlined the importance of this dynamic of Shared Anthropology :« …in Jean Rouch's longstanding commitment to and development of film as a vehicle for the creation of a "shared anthropology," in research, in production, in exhibition, in pedagogy, and in social action. First and foremost is his concern that one's knowledge about another culture be produced in a way that can be shared with members of that culture. » 7

As students we were privileged as Rouch gave us the possibilities to meet and exchange with Tim Ash, Colin Young, Bob Gardner, John Marshall, Raymond Depardon, Michel Brault….

After the "Saturday morning" class at the Cinematheque which was part of the DEA and PHD 5 Meyer Fortes 1906-1983. As anthropologist he worked among the Ashanti and Tallensi in Ghana and spent most of his career at Cambridge University and he was the Willima Wyse Professor of Social Anthropology. 6 The parallax effect : The Impact of Aboriginal Media on Ethnographic film.Visual Anthropology Review, Volume 11, Number 2, Fall 1995 7 idem program, we shared lunch together and started lively discussions on films and projects real or imaginary… As the Cinéma du Réel created in 1978 was rejecting films classified as ethnographic, Rouch became so upset he decided to create his own festival. In 1982, with Françoise Foucault they set up the frame and the informal team around the Ethnographic Film Committee, and started the event called le Bilan. The main idea was to have the freedom to present films which didn't necessarily meet the criteria for TV classification or even for professional standards.

During this period, students working on a PHD in Visual Anthropology were filming in Super8, a format that wasn't recognised as a professional one. For Rouch, quality comes from the ways of looking, ways of establishing the relationship with the people being filmed and in your abilityto render this relationship on screen. Always sitting in the second row on the left side of the Museum of Mankind, Rouch would admire the grain, the dust, the smell of the film. It was crucial to present filmswhich didn't fit the official format recognised by other festivals. He encouraged innovative approaches and fostered new styles among filmmakers, ethnographers and students in visual anthropology.

By recalling these two events, from their creation until today's evolution, I would like to emphasize the role of these festivals in the academic landscape of this periodandalso the importance of funding in relation to the freedom of the Ethnographic Film Committee and to the spirit of these key moments in the visual anthropology network.

The Bilan was a significant encounterfor the visual anthropology network. Colleagues from the Institut für den Wissenschaftlichen Film in Göttingen, from the National Film and Television School, from Leiden University came with their students or participated as filmmakers (Peter Crawford, Beate Englebrecht, Paul Henley, Heimo Lapapleilen,, Dirk Nijland…). The Bilan gave rise to other manifestations such as the one in Göttingen in 1993.

One of the specificities of the Bilan was the funding process. As Rouch and Françoise Foucault were both paid by the CNRS, they dedicated their time to organising such events. The main cost was receiving and sending back the prints. The Committee received significant assistance with the diplomatic bag, accessible and ready to support in an informal way such events. The students, involved in a very easy-going way, were also completely dedicated to the event. They were happy to help just for the pleasure of sharing such encounters. Sometimes, the Committee was confronted with unexpected difficulties and Philippe Lourdou and myself were once told, a day before the event, that we'd have to manage the screenings and deal with the 35mm the 16mm or Super8mm projectors…. So much fun and such good memories;the singular feelingof being part of an informal team united by Jean Rouch's spirit and his insatiable desire to share knowledge, ways of life, ways of building bridges between people from all over the world.

By writing these lines in Paris in 2015, I really feel we should find within ourselves the means to re-inject into the world the marvelous utopian energy that Rouch shared with us.

Of course, some researchers from the CNRS and even University professors continued to ignore such events and Rouch andFulchignoni had to fight against the academic system in order to create a space of expression for the students who make films as publications, and pursue film as a career.

Rouch was profoundly interested in creating moments and spaces for exchanging ideas and creativity, offering opportunities to reinvent the world. Each event, by being held repeatedly over years, wasinevitably taken up by theofficial systems and integrated slowly into the norm. It's not a question of quality or originality but of social dynamic, and as soon as a platform becomes part of official programmes, it looses at some point its role as a pioneer.

In this spirit, in 2012 we created as part of the Bilan a new section called Narrativités Singulières in order to open the space for people questioning the linearity of the audiovisualmediumand for people dealing with programming language as a tool of expression. The manifestation is organised in a Digital Art Center called Le Cube; it invites people concerned with this dynamic to break through the norms of the prevailing academic system andclaim the key role of creation as a methodology. I can hear Rouch's voice,saying one more time,'Cric Crac'… as if he is still provoking us and inviting us to breathe new creative energies into our work and to "détourne" tiressly all new forms of constraint that are imposed by the current socio-economic system. From 2012, she conceived with colleagues of her, a manifestation " Digital anthropologies" in Le Cube, Digital Art Centre. She is the chief editor of Anthrovision, online journal of the Vaneasa network.

  Short Bio: N Wanono, former PHD student of Jean Rouch; she worked with him during her field work among the Dogon and also during the Mozambique workshop organised in the 78. She is actually tenure researcher at the CNRSIMAF. She produced several films and co directed with Philippe Lourdou In the Shadow of the Sun, funeral and enthronement of the Hogon of Arou,83mn, Arte 1997. She co edited a book: Creation and diffusion in Visual anthropology.

The initiators of this event were, J.M Arnold, Secrétaire Général des rencontres de l'Audiovisuel scientifique, director of the Serdav puis du CNRS AV, Mariel Delorme, in charge of the manifestations at the Serddav puis au CNRSAV, J.Rouch, Genral Secretary of the Ethnographic Film Committee.

A.Leroi-Gourhan, "cinéma et sciences humaines-Le film ethnologique existe-t-il ? "La revue de géographie humaine et d'ethnologie n̊3, 1948..." 3 The parallax effect : The Impact of Aboriginal Media on Ethnographic film. Visual Anthropology Review,Volume 11, Number 2, Fall 1995

Georges Henri Rivière 1897-1985. He founded the Musée des Arts et Traditions Populaires in Paris. In 1936, he reorganised with Paul Rivet, the Musée Ethnographique du Trocadera which became Le Musée de l'Homme

This first offer of training in Cinema and documentary in a French University serves as an anchor in the French academic system. In 1971, Jean Rouch created a research centre, "La FRC" (diploma was recognised by both universities Paris I -La Sorbonne and Paris Xinternational documentary film festival organised at the Pompidou Centre