Rely-guarantee protocols for safe interference over shared memory

Mutable state can be useful in certain algorithms, to structure programs, or for efficiency purposes. However, when shared mutable state is used in non-local or nonobvious ways, the interactions that can occur via aliases to that shared memory can be a source of program errors. Undisciplined uses of shared state may unsafely interfere with local reasoning as other aliases may interleave their changes to the shared state in unexpected ways. We propose a novel technique, rely-guarantee protocols, that structures the interactions between aliases and ensures that only safe interference is possible. We present a linear type system outfitted with our novel sharing mechanism that enables controlled interference over shared mutable resources. Each alias is assigned separate, local roles encoded in a protocol abstraction that constrains how an alias can legally use that shared state. By following the spirit of rely-guarantee reasoning, our rely-guarantee protocols ensure that only safe interference can occur but still allow many interesting uses of shared state, such as going beyond invariant and monotonic usages. This thesis describes the three core mechanisms that enable our type-based technique to work: 1) we show how a protocol models an alias’s perspective on how the shared state evolves and constrains that alias’s interactions with the shared state; 2) we show how protocols can be used while enforcing the agreed interference contract; and finally, 3) we show how to check that all local protocols to some shared state can be safely composed to ensure globally safe interference over that shared memory. The interference caused by shared state is rooted at how the uses of di↵erent aliases to that state may be interleaved (perhaps even in non-deterministic ways) at run-time. Therefore, our technique is mostly agnostic as to whether this interference was the result of alias interleaving caused by sequential or concurrent semantics. We show implementations of our technique in both settings, and highlight their di↵erences. Because sharing is “first-class” (and not tied to a module), we show a polymorphic procedure that enables abstract compositions of protocols. Thus, protocols can be specialized or extended without requiring specific knowledge of the interference produce by other protocols to that state. We show that protocol composition can ensure safety even when considering abstracted protocols. We show that this core composition mechanism is sound, decidable (without the need for manual intervention), and provide an algorithm implementation.

Novel MLPA procedure using self-designed probes allows comprehensive analysis for CNVs of the genes involved in Hirschsprung disease.

Background: Hirschsprung disease is characterized by the absence of intramural ganglion cells in the enteric plexuses, due to a fail during enteric nervous system formation. Hirschsprung has a complex genetic aetiology and mutations in several genes have been related to the disease. There is a clear predominance of missense/nonsense mutations in these genes whereas copy number variations (CNVs) have been seldom described, probably due to the limitations of conventional techniques usually employed for mutational analysis. In this study, we have looked for CNVs in some of the genes related to Hirschsprung (EDNRB, GFRA1, NRTN and PHOX2B) using the Multiple Ligation-dependent Probe Amplification (MLPA) approach. Methods: CNVs screening was performed in 208 HSCR patients using a self-designed set of MLPA probes, covering the coding region of those genes. Results: A deletion comprising the first 4 exons in GFRA1 gene was detected in 2 sporadic HSCR patients and in silico approaches have shown that the critical translation initiation signal in the mutant gene was abolished. In this study, we have been able to validate the reliability of this technique for CNVs screening in HSCR. Conclusions: The implemented MLPA based technique presented here allows CNV analysis of genes involved in HSCR that have not been not previously evaluated. Our results indicate that CNVs could be implicated in the pathogenesis of HSCR, although they seem to be an uncommon molecular cause of HSCR.

Direct visualization of the trimeric structure of the ASIC1a channel, using AFM imaging.

There has been confusion about the subunit stoichiometry of the degenerin family of ion channels. Recently, a crystal structure of acid-sensing ion channel (ASIC) 1a revealed that it assembles as a trimer. Here, we used atomic force microscopy (AFM) to image unprocessed ASIC1a bound to mica. We detected a mixture of subunit monomers, dimers and trimers. In some cases, triple-subunit clusters were clearly visible, confirming the trimeric structure of the channel, and indicating that the trimer sometimes disaggregated after adhesion to the mica surface. This AFM-based technique will now enable us to determine the subunit arrangement within heteromeric ASICs.

Film-free laser forward printing of transparent and weakly absorbing liquids

A laser-based technique for printing transparent and weakly absorbing liquids is developed. Its principle of operation relies in the tight focusing of short laser pulses inside the liquid and close to its free surface, in such a way that the laser radiation is absorbed in a tiny volume around the beam waist, with practically no absorption in any other location along the beam path. If the absorbed energy overcomes the optical breakdown threshold, a cavitation bubble is generated, and its expansion results in the propulsion of a small fraction of liquid which can be collected on a substrate, leading to the printing of a microdroplet for each laser pulse. The technique does not require the preparation of the liquid in thin film form, and its forward mode of operation imposes no restriction concerning the optical properties of the substrate. These characteristics make it well suited for printing a wide variety of materials of interest in diverse applications. We demonstrate that the film-free laser forward printing technique is capable of printing microdroplets with good resolution, reproducibility and control, and analyze the influence of the main process parameter, laser pulse energy. The mechanisms of liquid printing are also investigated: time-resolved imaging provides a clear picture of the dynamics of liquid transfer which allows understanding the main features observed in the printed droplets.

Human melanoma-specific CD8(+) T-cells from metastases are capable of antigen-specific degranulation and cytolysis directly ex vivo.

The relatively low frequencies of tumor Ag-specific T-cells in PBMC and metastases from cancer patients have long precluded the analysis of their direct ex vivo cytolytic capacity. Using a new composite technique that works well with low cell numbers, we aimed at determining the functional competence of melanoma-specific CD8(+) T-cells. A multiparameter flow cytometry based technique was applied to assess the cytolytic function, degranulation and IFNγ production by tumor Ag-specific CD8(+) T-cells from PBMC and tumor-infiltrated lymph nodes (TILN) of melanoma patients. We found strong cytotoxicity by T-cells not only when they were isolated from PBMC but also from TILN. Cytotoxicity was observed against peptide-pulsed target cells and melanoma cells presenting the naturally processed endogenous antigen. However, unlike their PBMC-derived counterparts, T-cells from TILN produced only minimal amounts of IFNγ, while exhibiting similar levels of degranulation, revealing a critical functional dichotomy in metastatic lesions. Our finding of partial functional impairment fits well with the current knowledge that T-cells from cancer metastases are so-called exhausted, a state of T-cell hyporesponsiveness also found in chronic viral infections. The identification of responsible mechanisms in the tumor microenvironment is important for improving cancer therapies.

EEG windowed statistical wavelet scoring for evaluation and discrimination of muscular artifacts

EEG recordings are usually corrupted by spurious extra-cerebral artifacts, which should be rejected or cleaned up by the practitioner. Since manual screening of human EEGs is inherently error prone and might induce experimental bias, automatic artifact detection is an issue of importance. Automatic artifact detection is the best guarantee for objective and clean results. We present a new approach, based on the time–frequency shape of muscular artifacts, to achieve reliable and automatic scoring. The impact of muscular activity on the signal can be evaluated using this methodology by placing emphasis on the analysis of EEG activity. The method is used to discriminate evoked potentials from several types of recorded muscular artifacts—with a sensitivity of 98.8% and a specificity of 92.2%. Automatic cleaning ofEEGdata are then successfully realized using this method, combined with independent component analysis. The outcome of the automatic cleaning is then compared with the Slepian multitaper spectrum based technique introduced by Delorme et al (2007 Neuroimage 34 1443–9).

Detection of genetically modified organisms in soy products sold in Turkish market

PCR-based technique for GMO detection is the most reliable choice because of its high sensitivity and specificity. As a candidate of the European Union, Turkey must comply with the rules for launching into the market, traceability, and labeling of GMOs as established by EU legislation. Therefore, the objective of this study is to assess soybean products in the Turkish market to verify compliance with legislation using qualitative Polymerase Chain Reaction (PCR) assay to detect the presence of GM soybean and to quantify its amount of GM soybean in the samples tested positive using real-time PCR. DNA extracted by the modified CTAB method was properly used for PCR amplification of food materials. The amplification of a 118 bp DNA fragment of the lectin gene from soybean by PCR was successfully achieved in all samples. The GMO screening was based on the detection of 35S promoter and NOS terminator sequences. The GM positive samples were subjected to detection of Roundup ReadyTM soybean (RR) using quantitative real-time PCR. It was found that 100% of the tested food samples contained less than 0.1 per cent of EPSPS gene.

The analysis of gene transcripts associated with conidiation in the insect pathogenic fungus, Metarhizium anisopliae /

Conidia of the insect pathogenic fungus, Metarhizium anisopliae play an important role in pathogenicity because they are the infective propagules that adhere to the surface of the insect, then germinate and give rise to hyphal penetration of the insect cuticle. Conidia are produced in the final stages of insect infection as the mycelia emerge from the insect cadaver. The genes associated with conidiation have not yet been studied in this fiingus. hi this study we used the PCR-based technique, suppression subtractive hybridization (SSH) to selectively amplify conidial-associated genes in M. anisopliae. We then identified the presence of these differentially expressed genes using the National Center for Biotechnology Information database. One of the transcripts encoded an extracellular subtilisin-like protease, Prl, which plays a fundamental role in cuticular protein degradation. Analysis of the patterns of gene expression of the transcripts using RT-PCR indicated that conidial-associated cDNAs are expressed during the development of the mature conidium. RT-PCR analysis was also performed to examine in vivo expression of Prl during infection of waxworm larvae {Galleria mellonelld). Results showed expression of Prl as mycelia emerge and produce conidia on the surface of the cadaver. It is well documented that Prl is produced during the initial stages of transcuticular penetration by M. anisopliae. We suggest that upregulation of Prl is part of the mechanism by which reverse (from inside to the outside of the host) transcuticular penetration of the insect cuticle allows subsequent conidiation on the cadaver.

Développement d’un instrument d’évaluation des besoins de réadaptation des personnes atteintes de maladies respiratoires chroniques

La réadaptation pulmonaire est une intervention dont l’efficacité est largement reconnue. Cette efficacité a été établie grâce à l’utilisation d’instruments de mesure d’impact global. Les patients bénéficiant des programmes de réadaptation pulmonaire possèdent des caractéristiques variées et souffrent généralement de maladie pulmonaire obstructive chronique à différents degrés. En fonction de leurs différents besoins, les patients répondent de façon variable aux composantes d’un programme de réadaptation pulmonaire. Il est recommandé d’individualiser les programmes en fonction des besoins des patients afin d’en optimiser les effets. À cette fin, l’évaluation des besoins de réadaptation des patients est nécessaire. Comme il n’existe actuellement aucun instrument standardisé pour procéder à cette évaluation, nous avons entrepris d’en développer un à l’aide de méthodes qualitatives et quantitatives de recherche. Un modèle conceptuel d’évaluation des besoins de réadaptation des patients a été élaboré suite aux résultats tirés de groupes de discussion, de la consultation de dossiers médicaux et d’une recension des écrits. À partir de ce modèle, des items devant être sélectionnés de façon individualisée parmi cinq domaines (reconnaissance des besoins, connaissance, motivation, attentes et buts) ont été pré-testés. Les tendances générales concernant la validité des items contenus dans le prototype d’instrument ont été vérifiées lors d’une étude pilote auprès de 50 répondants en réadaptation. Les pistes d’investigation dégagées dans ce mémoire serviront aux études de validation plus approfondies dont devrait faire l’objet ce prototype d’instrument dans le futur.

Effets des nanoparticules d'argent sur les processus enzymatiques des sols

Les nanomatériaux sont de plus en plus présents dans les produits consommables du quotidien. L’argent est le métal le plus utilisé en nanotechnologie pour ses propriétés antimicrobiennes. Par différentes voies d’entrée, les nanoparticules d’argent (nAg) se retrouvent dans l’environnement en quantité significative, notamment dans les sols suite à la valorisation agricole des biosolides municipaux. Il est prévu qu’une interaction négative sur la communauté microbienne terrestre ait des répercussions sur la fertilité du sol et les processus biogéochimiques. Les mesures de l’activité enzymatique ont déjà montré leur efficacité et leur sensibilité dans la détection d’une perturbation physique et chimique du sol. Les effets potentiels des nAg sur l’écosystème terrestre ont été évalués en mesurant l’activité des enzymes β-D-glucosidase (EC 3.2.1.21), leucine-aminopeptidase (EC 3.4.11.1), phosphomonoesterase (EC 3.1.3) et arylsulfatase (EC 3.1.6.1) intervenant dans les cycles des éléments essentiels C, N, P et S, respectivement. L’activité enzymatique est mesurée à l’aide d’une technique basée sur la fluorescence qui requière des substrats synthétiques liés à un fluorophore. Un sol de type sableux a été échantillonné au Campus Macdonald de l’Université McGill (Sainte-Anne-de-Bellevue, Qc) puis exposé aux nAg (taille ~20 nm) ou à la forme ionique Ag+ (Ag-acetate) à des concentrations nominales de 1,25 × 10-3, 1,25 × 10-2, 0,125, 1,25, 6,25 et 31,25 mg Ag kg-1 sol. De plus, le rôle de la matière organique (MO) a été évalué en effectuant un amendement du sol avec un compost de feuilles. Pour mieux comprendre les effets observés, des analyses de spéciation de l’Ag ont été réalisées. Les concentrations en Ag dissous ont été déterminées après filtration à travers des membranes de 0,45 µm ou de 3 kDa (~1 nm, ultrafiltration) pour séparer la phase particulaire des ions dissous. De façon générale, une inhibition de l’activité enzymatique a été observée pour les 4 enzymes en fonction de l’augmentation de la concentration en Ag (totale et dissoute) mais elle est significativement moins importante avec l’ajout de la MO. Les résultats suggèrent que l’inhibition de l’activité des enzymes aux faibles expositions aux nAg est due aux nanoparticules puisqu’une très faible fraction des nAg est réellement dissoute et aucun effet significatif n’a été observé pour les sols traités à des concentrations similaires en Ag+. Par contre, les effets mesurés aux concentrations plus élevées en nAg sont semblables aux expositions à l’Ag+ et suggèrent un rôle de l’Ag colloïdale dans l’inhibition du processus enzymatique des sols.

Improving automation in model-driven engineering using examples

Cette thèse a pour but d’améliorer l’automatisation dans l’ingénierie dirigée par les modèles (MDE pour Model Driven Engineering). MDE est un paradigme qui promet de réduire la complexité du logiciel par l’utilisation intensive de modèles et des transformations automatiques entre modèles (TM). D’une façon simplifiée, dans la vision du MDE, les spécialistes utilisent plusieurs modèles pour représenter un logiciel, et ils produisent le code source en transformant automatiquement ces modèles. Conséquemment, l’automatisation est un facteur clé et un principe fondateur de MDE. En plus des TM, d’autres activités ont besoin d’automatisation, e.g. la définition des langages de modélisation et la migration de logiciels. Dans ce contexte, la contribution principale de cette thèse est de proposer une approche générale pour améliorer l’automatisation du MDE. Notre approche est basée sur la recherche méta-heuristique guidée par les exemples. Nous appliquons cette approche sur deux problèmes importants de MDE, (1) la transformation des modèles et (2) la définition précise de langages de modélisation. Pour le premier problème, nous distinguons entre la transformation dans le contexte de la migration et les transformations générales entre modèles. Dans le cas de la migration, nous proposons une méthode de regroupement logiciel (Software Clustering) basée sur une méta-heuristique guidée par des exemples de regroupement. De la même façon, pour les transformations générales, nous apprenons des transformations entre modèles en utilisant un algorithme de programmation génétique qui s’inspire des exemples des transformations passées. Pour la définition précise de langages de modélisation, nous proposons une méthode basée sur une recherche méta-heuristique, qui dérive des règles de bonne formation pour les méta-modèles, avec l’objectif de bien discriminer entre modèles valides et invalides. Les études empiriques que nous avons menées, montrent que les approches proposées obtiennent des bons résultats tant quantitatifs que qualitatifs. Ceux-ci nous permettent de conclure que l’amélioration de l’automatisation du MDE en utilisant des méthodes de recherche méta-heuristique et des exemples peut contribuer à l’adoption plus large de MDE dans l’industrie à là venir.

A Mono- and Multi-objective Approach for Recommending Software Refactoring

Les systèmes logiciels sont devenus de plus en plus répondus et importants dans notre société. Ainsi, il y a un besoin constant de logiciels de haute qualité. Pour améliorer la qualité de logiciels, l’une des techniques les plus utilisées est le refactoring qui sert à améliorer la structure d'un programme tout en préservant son comportement externe. Le refactoring promet, s'il est appliqué convenablement, à améliorer la compréhensibilité, la maintenabilité et l'extensibilité du logiciel tout en améliorant la productivité des programmeurs. En général, le refactoring pourra s’appliquer au niveau de spécification, conception ou code. Cette thèse porte sur l'automatisation de processus de recommandation de refactoring, au niveau code, s’appliquant en deux étapes principales: 1) la détection des fragments de code qui devraient être améliorés (e.g., les défauts de conception), et 2) l'identification des solutions de refactoring à appliquer. Pour la première étape, nous traduisons des régularités qui peuvent être trouvés dans des exemples de défauts de conception. Nous utilisons un algorithme génétique pour générer automatiquement des règles de détection à partir des exemples de défauts. Pour la deuxième étape, nous introduisons une approche se basant sur une recherche heuristique. Le processus consiste à trouver la séquence optimale d'opérations de refactoring permettant d'améliorer la qualité du logiciel en minimisant le nombre de défauts tout en priorisant les instances les plus critiques. De plus, nous explorons d'autres objectifs à optimiser: le nombre de changements requis pour appliquer la solution de refactoring, la préservation de la sémantique, et la consistance avec l’historique de changements. Ainsi, réduire le nombre de changements permets de garder autant que possible avec la conception initiale. La préservation de la sémantique assure que le programme restructuré est sémantiquement cohérent. De plus, nous utilisons l'historique de changement pour suggérer de nouveaux refactorings dans des contextes similaires. En outre, nous introduisons une approche multi-objective pour améliorer les attributs de qualité du logiciel (la flexibilité, la maintenabilité, etc.), fixer les « mauvaises » pratiques de conception (défauts de conception), tout en introduisant les « bonnes » pratiques de conception (patrons de conception).

Création interactive de mondes virtuels : combiner génération procédurale et contrôle utilisateur intuitif

Réalisé en cotutelle avec l'Université de Grenoble.

Une approche heuristique pour l’apprentissage de transformations de modèles complexes à partir d’exemples

L’ingénierie dirigée par les modèles (IDM) est un paradigme d’ingénierie du logiciel bien établi, qui préconise l’utilisation de modèles comme artéfacts de premier ordre dans les activités de développement et de maintenance du logiciel. La manipulation de plusieurs modèles durant le cycle de vie du logiciel motive l’usage de transformations de modèles (TM) afin d’automatiser les opérations de génération et de mise à jour des modèles lorsque cela est possible. L’écriture de transformations de modèles demeure cependant une tâche ardue, qui requiert à la fois beaucoup de connaissances et d’efforts, remettant ainsi en question les avantages apportés par l’IDM. Afin de faire face à cette problématique, de nombreux travaux de recherche se sont intéressés à l’automatisation des TM. L’apprentissage de transformations de modèles par l’exemple (TMPE) constitue, à cet égard, une approche prometteuse. La TMPE a pour objectif d’apprendre des programmes de transformation de modèles à partir d’un ensemble de paires de modèles sources et cibles fournis en guise d’exemples. Dans ce travail, nous proposons un processus d’apprentissage de transformations de modèles par l’exemple. Ce dernier vise à apprendre des transformations de modèles complexes en s’attaquant à trois exigences constatées, à savoir, l’exploration du contexte dans le modèle source, la vérification de valeurs d’attributs sources et la dérivation d’attributs cibles complexes. Nous validons notre approche de manière expérimentale sur 7 cas de transformations de modèles. Trois des sept transformations apprises permettent d’obtenir des modèles cibles parfaits. De plus, une précision et un rappel supérieurs à 90% sont enregistrés au niveau des modèles cibles obtenus par les quatre transformations restantes.

A unified framework for the comprehension of software's time dimension

Les logiciels sont de plus en plus complexes et leur développement est souvent fait par des équipes dispersées et changeantes. Par ailleurs, de nos jours, la majorité des logiciels sont recyclés au lieu d’être développés à partir de zéro. La tâche de compréhension, inhérente aux tâches de maintenance, consiste à analyser plusieurs dimensions du logiciel en parallèle. La dimension temps intervient à deux niveaux dans le logiciel : il change durant son évolution et durant son exécution. Ces changements prennent un sens particulier quand ils sont analysés avec d’autres dimensions du logiciel. L’analyse de données multidimensionnelles est un problème difficile à résoudre. Cependant, certaines méthodes permettent de contourner cette difficulté. Ainsi, les approches semi-automatiques, comme la visualisation du logiciel, permettent à l’usager d’intervenir durant l’analyse pour explorer et guider la recherche d’informations. Dans une première étape de la thèse, nous appliquons des techniques de visualisation pour mieux comprendre la dynamique des logiciels pendant l’évolution et l’exécution. Les changements dans le temps sont représentés par des heat maps. Ainsi, nous utilisons la même représentation graphique pour visualiser les changements pendant l’évolution et ceux pendant l’exécution. Une autre catégorie d’approches, qui permettent de comprendre certains aspects dynamiques du logiciel, concerne l’utilisation d’heuristiques. Dans une seconde étape de la thèse, nous nous intéressons à l’identification des phases pendant l’évolution ou pendant l’exécution en utilisant la même approche. Dans ce contexte, la prémisse est qu’il existe une cohérence inhérente dans les évènements, qui permet d’isoler des sous-ensembles comme des phases. Cette hypothèse de cohérence est ensuite définie spécifiquement pour les évènements de changements de code (évolution) ou de changements d’état (exécution). L’objectif de la thèse est d’étudier l’unification de ces deux dimensions du temps que sont l’évolution et l’exécution. Ceci s’inscrit dans notre volonté de rapprocher les deux domaines de recherche qui s’intéressent à une même catégorie de problèmes, mais selon deux perspectives différentes.