Skip to topic | Skip to bottom
Home
Linfo
Linfo.RapportEcritr1.19 - 24 Jun 2005 - 11:58 - BenychouSabrinatopic end

Start of topic | Skip to actions

Résumé

Ce travail d'étude traite des méthodes possibles au sujet la gestion des ressources informatiques lors des problèmes de concurrence.
Nous présentons les moyens de résolution et de preuves connues à notre niveau, puis après avoir présenté l'outil qu'est la logique linéaire, nous l'appliquons dans le cadre de la concurrence.
Actuellement, lors de problèmes de partage de ressources par des processus nous pouvons placer des drapeaux, des sémaphores, des moniteurs dans les programmes de ces derniers afin de départager qui utilisera quoi.
Malheureusement, nous avons peu de chances de détecter les exclusions mutuelles et risque de famine avant que le programme ne soit lancé et bloqué.
Sur les problèmes simples, nous pourrons toujours tester les principaux cas difficiles connus, mais là encore nous pouvons en oublier.
C'est bien dans le soucis de clarifier ces boîtes noires que sont les protocoles d'entrée et de sortie en section critique que nous avons cherché une nouvelle formalisation.
La logique linéaire découverte par M Jean Yves Girard en 1985 répond bien à cette attente.
En effet, la logique matière clé du raisonnement mécanique est et reste le fondement de l'architecture des ordinateurs, bit à bit , mot à mot, bus à bus le processeur ne connait qu'une suite d'opérations régies par les lois de Morgan.
Il n'est donc pas innocent de choisir ce domaine pour résoudre ces problèmes de raisonnement informatique avec un modèle logique.
Mais les logiques incluant les lois de Morgan et la notion de ressources épuisables ne sont ni courantes ni à la mode.
Par sa structure la logique linéaire va nous permettre d'ajouter cette notion de consommation des ressources.
L'équilibre est le mot clé des équations écrites avec cette dernière.
Ainsi si nous avons deux imprimantes après réecriture il en restera deux.
Cette logique se construisant par preuves nous permettra de tester les solutions trouvées et de corriger les algorithmes avant même leur implémentation.
Mais cet outil terriblement riche ne pourra pas être décrit dans son ensemble.
Nous n'en présenterons que quelques points utiles pour développer notre exemple.

plan et code latex

  • Introduction
    • Définition d'une ressource * Introduction à la concurrence et ses outils
      • Les philosophes
      • Le problème des Trains Boliviens et Péruviens
    • Résolution des problèmes
      • sémaphores
      • moniteurs
  • La logique linéaire
    • La Logique Propositionnelle
      • Présentation des séquents
      • Présentation des règles
        • affaiblissement
        • réduction
        • introduction
        • contraction
      • Limites de cette logique pour la concurrence
        • affaiblissement
        • réduction
      • Finesse d'une autre logique (intuitions)
        • la conjonction transformé en 2 symboles (le "et" et le "par") : exemples
        • la disjonction transformé en 2 symboles (le "ou" et le "avec") : exemples
    • Vers la logique linéaire
      • Histoire de la logique linéaire
        • Hilbert : notion de démonstration
        • Hauptsak : traduction de la logique classique dans la logique intuitionniste
        • Lewis Carroll : théorème de déduction des séquents
      • Tentatives de formalisations de la logique propositionnelle vers la logique linéaire
        • Exemple des croissants et des pains au chocolat : formalisation et présentation des symboles
    • Logique Linéaire, une logique de ressources?
      • Présentation des connecteurs : exemple des menus
      • Présentation des éléments duals : la négation
      • Récapitulatif des différents connecteurs
  • Mise en oeuvre de la logique linéaire
    • Notion d'équilibre
      • affaiblissement
      • réduction
    • Formalisation
      • Règles d'introduction
      • Axiomes et réseaux de preuves
    • Illustration avec les philosophes
    • Réseaux de Pétri et Logique Linéaire
    • application des réseaux de Pétri: les trains ou les lecteurs/rédacteurs
  • Autres Applications de la Logique Linéaire
    • Linguistique
    • Programmation fonctionnelle
    • Programmation logique
  • Conclusion


to top

I Attachment sort Action Size Date Who Comment
TEnouveau1.zip manage 91.2 K 02 May 2005 - 13:37 EspenelCeline  
TE2.zip manage 673.4 K 10 May 2005 - 13:39 BenychouSabrina fichiers latex
TE3.zip manage 1105.0 K 29 May 2005 - 20:15 BenychouSabrina version avec graphiques
rapport-pdf.pdf manage 527.7 K 24 Jun 2005 - 11:57 BenychouSabrina derniere version
TE6.zip manage 1273.7 K 23 Jun 2005 - 22:46 BenychouSabrina  

You are here: Linfo > JournauxDeBord > GestionDesRessources > RapportEcrit

to top

Copyright © 1999-2019 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding WIKIDeptinfo? Send feedback