Encore un peu de topologie en Coq

Seconde partie sur la série autour de quelques preuves d’exercices classiques de topologie en Coq, on va s’attaquer cette fois encore à un exercice de « réécriture » de définitions, toujours tiré de la même feuille d’exercice :

Soit \(X\) un ensemble non vide et \(\Sigma\) une famille de parties de \(X\) stable par intersection finie et contenant \(X\). Montrer que la plus petite topologie \(T\) contenant \(\Sigma\) (la topologie engendrée par \(\Sigma\)) est constituée des unions d’ensembles de \(\Sigma\), ou, de façon équivalente,
\(A\in T \iff \forall x\in A, \exists S \in \Sigma, x\in S \subset A\)
Montrer que l’on peut affaiblir l’hypothèse de stabilité par intersection finie en :
\(\forall S_1, S_2 \in \Sigma, \forall S \in S_1 \cap S_2, \exists S_3 \in \Sigma, x\in S_3 \subset S_1 \cap S_2\).

Là encore on va faire son marché parmi les choses qu’on veut démontrer : en particulier la première partie me semble pas particulièrement passionnante (c’est compliqué pour toutes les topologies y compris la plus petite de pas contenir au moins les unions d’ensemble) et donc on va passer directement à l’hypothèse affaiblie ; il suffit 1 de prouver que cette hypothèse combinée à la stabilité par union implique la stabilité par intersection finie.

En Coq

Dans le code on utilisera la lettre S pour désigner \(\Sigma\)2.

La stabilité par union est relativement simple à écrire:

Definition hypothese_union (T:Type) (S:Family T) :=
    forall S', Included S' S -> S (FamilyUnion S').

De même que l’hypothèse affaiblie de l’énoncé, qui n’est qu’une traduction avec les mots clés Coq qui vont bien :

Definition hypothese_afaiblie (T:Type) (S:Family T) :=
    forall (S1 S2:Ensemble T), 
    In S S1 ->
    In S S2 ->
    forall x, In (Intersection S1 S2) x ->
    (exists S3, In S S3 /\ In S3 x /\ Included S3 (Intersection S1 S2)).

Il faut cependant se méfier de l’apparente simplicité de ces définitions, un des écueils auxquels j’ai été confronté en rédigeant la preuve qui va suivre est la facilité avec laquelle on oublie d’expliciter une appartenance ou une inclusion dans un théorème, et donc casse les preuves qui en découlent.

Le théorème que l’on souhaite prouver :

Theorem exo:
    forall (T:Type) (S:Family T),
    hypothese_union T S ->
    hypothese_afaiblie T S ->
    (forall S1 S2, In S S1 -> In S S2 -> In S (Intersection S1 S2)). 
Proof.

Il peut être utile de prendre un peu de recul sur ce qu’on cherche à montrer : l’hypothèse affaiblie nous dit que, à défaut de stabilité « globale » par intersection finie, cette propriété vaut au moins localement. On peut alors s’en sortir en « découpant » une intersection en morceaux de S, et en réunissant ces morceaux grâces à l’hypothèse de stabilité par union.

Malheureusement je n’ai pas trouvé la plupart des théorèmes « intuitifs » sur les ensembles et leurs éléments dans le module zorns-lemma et il va donc falloir les écrire. Trouver quels sont les théorèmes dont on va avoir besoin est pas forcément facile et j’ai dû passer par pas mal de trial and errors avant de trouver comment m’en sortir, malgré l’apparente facilité de l’exercice.

Le  premier de ces théorèmes : si pour tout élément d’un ensemble E, on peut trouver un ensemble de S l’incluant, alors E est la réunion des éléments de S inclus dans E (si on n’avait pas l’hypothèse de l’implication, il aurait été possible d’avoir des « bouts qui manquent » dans E).

Qed.

Theorem union_of_elem (T:Type) (S:Family T) (E:Ensemble T):
  (forall x, In E x -> exists S', In S S' /\ In S' x /\ Included S' E) ->
  E=FamilyUnion (fun S' => In S S' /\ Included S' E).
Proof.

Là encore on est dans des manipulations de définition donc on va pas mal spammer la tactique unfold. La preuve se déroule alors relativement linéairement.

  intros. apply Extensionality_Ensembles. unfold Same_set. unfold Included in *. split.
  - unfold In. intros. destruct (H x H0). destruct H1. destruct H2.
    apply family_union_intro with (S:=x0). intros. split.
    + apply H1.
    + intros. apply H3. apply H4.
    +  apply H2.
  - intros. destruct H0. unfold In in *. destruct H0. apply H2. apply H1.
Qed.

Le second théorème est peut-être plus dispensable, je pense qu’il est possible de démontrer directement le résultat sur les intersections. Néanmoins par souci de clarté je le reproduis ici : il s’agit de montrer que rajouter l’hypothèse de stabilité des unions au théorème précédent fait que E est dans S :


Theorem function_app (T:Type) (S:Family T) (E:Ensemble T): 
  hypothese_union T S -> (forall x, In E x -> exists S', In S S' /\ In S' x /\ Included S' E) -> In S E.
Proof.

C’est surtout une application du théorème précédent:

  unfold hypothese_union. intros. pose (tmp:= union_of_elem T S E).
  rewrite tmp. apply H. unfold Included at 1. intros. destruct H1. apply H1. apply H0.
Qed.

Enfin la démonstration de l’exercice : ici il suffit de constater que le résultat précédent s’applique à une intersection d’éléments de S, sachant que l’hypothèse affaiblie est vérifiée. La preuve devient :

Proof.
  intros. apply function_app. apply H. intros. unfold hypothese_afaiblie in *. pose (tmp:= H0 S1 S2 H1 H2 x H3). destruct tmp. exists x0. apply H4.
Qed.


Un peu de topologie en Coq

Apprendre un langage de preuve est particulièrement déroutant quand on est habitué aux langages de programmations « classiques » qu’ils soient fonctionnels ou non : la plupart des patterns classiques deviennent perdent leur pertinence pour du code qui ne sera pas exécuté, et il faut adopter une façon différente de « penser » qui s’attachent aux propriétés des choses et non au comment de leur réalisation. Cependant s’il est difficile de transposer les pratiques de programmation pour s’entrainer à manipuler le langage, les maths fournissent beaucoup de matériau qui lui sied particulièrement bien (ce qui n’est pas surprenant). J’ai choisi de m’intéresser à la topologie dans cette série de billets pour voir jusqu’où il est possible d’aller. Je conseille fortement d’avoir lu au moins le premier tome de software foundation pour bien profiter de cette série.

Pour l’instant je m’inspire librement de https://github.com/coq-contribs/topology et en particulier je vais utiliser comme lui le module https://github.com/coq-contribs/zorns-lemma qui contient une implémentation des familles dénombrables ou non d’ensembles, de propriétés sur les fonctions etc. Il existe peut-être d’autres implémentation ailleurs mais je n’en ai pas trouvé.

Installation

Afin de pouvoir utiliser simplement les modules coq public, j’utilise le gestionnaire de paquets opam. Ce dernier n’est pas disponible nativement sur Windows actuellement, il faut donc passer par Windows Subsystem for Linux. L’installation se fait classiquement, via apt install m4 opam pour l’image Debian ou Ubuntu, m4 s’avérant parfois requis par certains paquets opam.

On utilise ensuite opam, qui va installer les paquets dans le répertoire de l’utilisateur, et modifier le fichier profile pour que bash puisse trouver l’exécutable Coq.

opam init
opam repo add coq-released http://coq.inria.fr/opam/released
opam install coq

Un premier exercice

Pour débuter, j’ai préféré rester modeste en choisissant un exercice relativement « tautologique » de topologie classique, trouvé sur cette liste : http://math.univ-lille1.fr/~bodin/exolic1/exolic.pdf :

Soit \(X\) un espace topologique, et \(f\) une application quelconque de \(X\) dans un ensemble \(Y\). On dit qu’une partie \(A\) de \(Y\) est ouverte, si \(f^{− 1}(A)\) est un ouvert de \(X\). Vérifier qu’on a défini ainsi une topologie sur \(Y\).

Sur les 3 axiomes définissant une topologie, celui sur l’appartenance de l’ensemble vide et de Y est relativement évident

1

, celui sur l’intersection fini est déjà défini dans zorns-lemma. Il reste donc l’axiome de stabilité par union.

Définitions d’ensemble, de réunion quelconque etc

La librairie standard de Coq propose une implémentation des ensembles https://coq.inria.fr/library/Coq.Sets.Ensembles.html : ces derniers contiennent juste une fonction d’appartenance de leur élément. On notera surtout la présence de l’axiome d’extensionalité (deux ensembles sont égaux s’ils sont inclus l’un dans l’autre) qu’on va utiliser dans la suite.

Coté zorns-lemma existe une définition de famille d’ensembles https://github.com/coq-contribs/zorns-lemma/blob/master/Families.v, qui correspond, de façon plutôt prévisible, à un alias sur les ensembles d’ensembles. Le type qui nous intéresse en particulier est celui de FamilyUnion, qui va « réduire » une famille en un ensemble. A noter que zorns-lemma propose aussi une version « indexed » des familles, version indexed qui, contrairement à ce que je pensais initialement, peut être indexée par n’importe quoi, et pas seulement par des entiers, et est probablement plus simple à manipuler ; cependant, dans la suite, je me base seulement sur le FamilyUnion classique.

On se lance

Premier point : définir l’ensemble réciproque d’une fonction. On pourrait certes utiliser la définition fournie par zorns-lemma, mais, vu que ce module ne fournit que très peu de propriétés sur les fonctions réciproques, le gain est minime.

From Topology Require Import TopologicalSpaces.

Definition img_recip (X Y:Type) (f:X->Y) (A: Ensemble Y) : Ensemble X:=

fun x => In A (f x).

Seconde étape, formuler l’égalité de l’union des images réciproques et de l’image réciproque de l’union. Pour plus de lisibilité, on va définir les deux séparément. D’un coté, on a l’image réciproque d’une union, relativement immédiate :

Definition img_recip_union (X Y:Type) (Fa: Family Y) (f:X->Y) :=

img_recip X Y f (FamilyUnion Fa).

De l’autre, on a la réunion des images réciproques, et c’est là où les choses commencent à se gâter. Si une FamilyUnion est une ensemble en premier lieu, il faut donc écrire une fonction d’appartenance, sauf que les éléments sont ici eux-mêmes des ensembles…dont la description nécessite quelques circonvolutions : il faut à la fois exprimer qu’on a l’image réciproque de quelque chose, et que ledit quelque chose est dans la famille de départ. J’avoue avoir galéré quelques temps avant de parvenir à écrire la définition, dont l’inélégance augure quelques prises de tête dans les futures preuves qui y seront rattachées :

Definition img_recip_union_as_fu (X Y:Type) (Fa: Family Y) (f:X->Y) : Ensemble X :=

FamilyUnion (fun S => exists F, In Fa F /\ S = (img_recip X Y f F)).

Il aurait probablement été plus simple de passer par les familles indexées (la faculté de « nommer » les ensembles qu’on manipule par leurs indices plutôt que par un quantifieur d’existence doit plutôt aider).

On pose enfin le théorème d’égalité des deux quantités :

Theorem union_img_inverse : forall (X Y : Type) (Fa:Family Y) (f:X->Y),

(img_recip_union_as_fu X Y Fa f) = (img_recip_union X Y Fa f).

Proof.

Comme énoncé préalablement, on reste sur un exercice plutôt tautologique, où on ne fait guère que renommer les choses. Par conséquent une grosse partie de la preuve va consister à utiliser en boucle la tactique unfold, qui va juste expliciter les définitions :

unfold img_recip_union_as_fu. unfold img_recip_union.

intros. unfold img_recip. unfold In.

On se retrouve avec une égalité entre deux ensembles.

apply Extensionality_Ensembles. split.

- unfold Included. unfold In. intros. destruct H eqn:Heqn. unfold In in i. destruct i eqn:ieqn. destruct a.

apply family_union_intro with (S:=x0). subst. apply f0. unfold In in i0. unfold In. subst. apply i0.

- unfold Included. intros. unfold In in H. Print FamilyUnion. remember (f x) as fx. destruct H.

eapply family_union_intro with (S:=fun x1 : X => S (f x1)). unfold In. exists S. split. apply H. trivial.

unfold In. rewrite <- Heqfx. apply H0.

Qed.

EMGU (OpenCV pour .Net) à la rescousse

Lors de mon précédent billet j’avais présenté comment utiliser les Windows Forms pour afficher une image. J’ai depuis découvert l’existence d’EMGU, un wrapper pour OpenCV qui fournit pas mal de fonctions utilitaires dont certaines pour charger et afficher des images. La plupart des fonctions usuelles de la bibliothèque sont disponibles de façon directe sous le namespace CvInvoke. Ainsi pour charger une image on utilisera imread comme suit :

open Emgu.CV

let img = CvInvoke.Imread(@ »C:\Users\vljno\Desktop\Canardcomission.png »)

Et pour l’afficher on utilisera imshow comme suit :

CvInvoke.Imshow(« nom de fenêtre », img)

CvInvoke.WaitKey(0)

Ce qui ne surprendra pas les personnes ayant déjà utilisé OpenCV dans d’autres langage.

Pour récupérer les données d’une image on utilisera le membre GetData de l’objet Mat retourné par Imread qui donnera un tableau 1d de bytes de l’image. A l’inverse, le membre SetTo permettra de changer le contenu de l’image.

img.GetData ([||])

img.SetTo someArray

Traitement d’image avec Fsharp et OpenCL

En ce moment je découvre les possibilités de F# en matière de scientific computing. F# (prononcé « Fsharp ») est un langage calqué sur OCaml dont il partage la syntaxe de base et une grosse partie de la bibliothèque standard. Quelques fonctionnalités disparaissent (les foncteurs et plus généralement tout ce qui concerne les modules, les types algébriques généralisés), des fonctionnalités sont légèrement retouchées (le quotation mark devient <@… @>, indentation non libre…), en contrepartie le langage a accès à la totalité de l’écosystème DotNet ou leur équivalent Mono et NetCore. Ces environnements étant particulièrement populaires il n’est pas étonnant de voir qu’il existe déjà des bibliothèques pour le calcul statistique, la recherche opérationnelle, les divers algorithmes d’intelligence artificielle, et pour ce qui nous concerne ici l’interfaçage avec des APIs de GPGPU comme OpenCL. Ce qui me donne l’occasion de tester les capacités de F# en tant que langage pour le traitement d’image face à un Python ou à un Matlab.

Commençons déjà par le code permettant de charger une image. De base DotNet fournit la classe Bitmap permettant de charger à peu près n’importe quel format courant et nous proposant d’accéder à ses pixels. Cette dernière est présente dans l’espace System.Drawing (dont il faudra référencer l’assembly) :

open System.Drawing
[<EntryPoint>]
let main argv =
    let img = new Bitmap(@"C:\Users\moi\Documents\fichier.jpg")
    // ….
    0

Afin de vérifier que tout se passe comme attendu il est souhaitable d’afficher cette image. Pour cela nous allons créer un System.Windows.Forms et dessiner l’image dedans via ce code :

open System.Windows.Forms
// ….
let form = new Form(Visible=true)
form.Paint.Add(function e-> e.Graphics.DrawImage(img, e.ClipRectangle, e.ClipRectangle, GraphicsUnit.Pixel))
System.Windows.Forms.Application.Run(form)

Si tout se passe bien vous devriez voir apparaitre votre image à l’écran dans une fenêtre relativement simple.

Maintenant que nous avons chargé notre image nous pouvons nous pencher sur l’utilisation d’OpenCL. Pour cela nous allons passer par la bibliothèque Brahma.OpenCL qui fournit à Fsharp une interface de relativement haut niveau autour d’OpenCL.Net. Cette dernière est disponible via Nuget.
L’initialisation de Brahma est relativement simple, il faut deux objets, un provider (qui représente votre installation OpenCL sur votre machine) et une CommandQueue à laquelle nous soumettrons les tâches que nous voulons effectuer :

open Brahma.OpenCL
open Brahma.FSharp.OpenCL.Core
open Brahma.FSharp.OpenCL.Extensions
open OpenCL.Net
open FSharp.Core
// ….
let provider = ComputeProvider.Create("*", DeviceType.Gpu)
let mutable commandQueue = new Brahma.OpenCL.CommandQueue(provider, provider.Devices |> Seq.head)

Ici nous utiliserons le premier GPU disponible, d’où le Seq.head.

L’avantage de Brahma.OpenCL est qu’elle repose sur les quotations marks pour la création de kernel OpenCL. Une quotation mark est un code F# sous forme d’arbre de syntaxe abstrait, ie une expression qui peut ensuite être passée comme argument à une fonction F#, par exemple pour la modifier, l’interpréter, ou dans le cas de Brahma, la traduire en code OpenCL. Ici nous allons écrire un filtre de Sobel (norme du gradient) prenant en argument un tableau 1d source et un tableau 1d destination (le gradient a besoin des informations des pixels l’entourant, il n’est pas possible de modifier « inplace » les données d’un tableau de façon concurrente. A noter que les quotations mark peuvent capturer des variables comme ici stride.

open Microsoft.FSharp.Quotations
// ….
let stride = img.Height;
let command = <@ fun (range:_2D) (buf:array<byte>) (dst:array<byte>) ->
    let i = range.GlobalID0
    let j = range.GlobalID1
    let mutable h = float32 0.
    if (i > 0 && i < stride) then
        let left = float32 buf.[i - 1 + stride * j]
        let right = float32 buf.[i + 1 + stride * j]
        h <- abs (left - right)
    let mutable v = float32 0.
    if (j > 0) then
        let top = float32 buf.[i + stride * (j - 1)]
        let bottom = float32 buf.[i + stride * (j + 1)]
        v <- abs (top - bottom)
    dst.[i + stride * j] <- byte (sqrt (h * h + v * v)) @>

Bien entendu il n’est pas possible d’écrire n’importe quel code, les kernels OpenCL ne pouvant pas être récursifs par exemple ou appeler des lambdas. La compilation d’une quotation mark sur du code qui ne peut être traduit génèrera une exception.

let kernel, kernelprepare, kernelrun = provider.Compile command

Les valeurs kernelprepare et kernelrun de la compilation permettent respectivement de mettre à disposition les dimensions et arguments (ici les tableaux buf et dst) du kernel au GPU, et d’exécuter ce code kernel via la syntaxe suivante :

kernelprepare d src dst
commandQueue.Add(kernelrun()) |> ignore
commandQueue.Add(dst.ToHost provider).Finish() |> ignore

d est un objet contenant les dimensions du workgroup (global et local) à utilizer pour le kernel, src et dst sont des Arrays F# classiques. On aura au préalable transféré le contenu 2d de img dans src 1d :

let d = _2D(img.Width, img.Height, 8, 8)
let src = Array.init (img.Width * img.Height) (function i -> img.GetPixel(i / stride, i % stride).R)
let dst = Array.zeroCreate (img.Width * img.Height)

Enfin une fois le kernel execute nous copions le contenu de dst dans img :

Array.iteri (fun i (v:byte) -> img.SetPixel(i / stride, i % stride, Color.FromArgb(255, int(v), int(v), int(v)))) dst

Voilà !

Emacs mode for VS 2017

Visual Studio 2008 had an Emacs mode that added most commonly used Emacs keybindings in the IDE. VS 2010 later made the feature available as an optional extension which unfortunaly wasn’t carried over on VS 2013. However the source of the extensions were published so that the communit could carry over : https://github.com/zbrad/EmacsKeys

Porting the extension to the latest version of Visual Studio is actually quite easy. It requires enabling Desktop DotNet and Visual Studio SDK feature in the installer though.

Out of the box the solution won’t compile because of missing assemblies : EnvDTE, Microsoft.VisualStudio.Shell.10*. EnvDTE references should be manually replaced by a reference to the envdte.dll assembly on the disk (in Program Files(x86)\Common Files\Microsoft Shared\MSEnv\PublicAssemblies\) ; I’m not sure why VS2017 doesn’t find it automatically to be honest seems it’s registered in a rather standard location.
Microsoft.VisualStudio.Shell.15 (there’s 2 versions available in the reference browser, both are needed) and Microsoft.VisualStudio.Shell.15.Framework will replace the reference to the older Shell.10 ones ; doing so will make the project target the 4.6.2 Framework.

The last piece of the port is to add a Prerequisites in the vsixmanifest file. I suggest adding the base IDE as the sole one.

Next the extension should build properly.

A note on Android physical security

My Android phone was stolen 2 weeks ago and unfortunatly the thieves were able to see my unlock pattern and thus to unlock it and access my gmail account. I could retrieve my account back thanks to google allowing password reset in case of dubious password change. I also hadn’t double authentication enabled which in such circumstance would have been annoying since I obviously couldn’t look at my phone messages anymore.

This leads me to write this small blog post gathering some advices in how to secure your accounts against physical phone access:

  • Use the fingerprints readers. I know it’s completely unreliable and fails nearly half of the time to detect your fingerprint but at least it’s unlikely to unlock without your own fingers.
  • Get a secondary mail account whose sole purpose is to serve as a password recovery option for your critical web accounts and NEVER access it from your phone or from a device you don’t own.
  • Critical web account obviously includes Samsung and/or Google one: since modern phone can be tracked remotely and includes a kill switch it’s the first thing that will be targeted. At least it happened in my case since I could see password reset notification from my Samsung account when I was back home and could restore my access to GMail.
  • Two-way authentication is becoming increasingly more popular. It’s probably very efficient to prevent security breach when accessing your account from a third party’s device but it’s also very dangerous if one has access to your phone. Having a spare phone line whose sole purpose is to serve as a second way authentication is likely costly; on the other hand, there are some physical alternative (like Yubi keys) which may be used instead. If you don’t accidently loose it.
  • Do regular backup since online service doesn’t always store every data or may need some obscure configuration to work as you may expect. For instance, I lost some of my text messages.
  • Don’t use the paypal mobile app. Never.
  • Don’t store any password PIN or credit card number as a clear text on your phone. If you have issue remembering a password, try to create one as a visual pattern on a keyboard. Muscle memory often works great in such case.
  • Even if unlock pattern are more secure than PIN number since there are at least 9! potential combination instead of 1000 numbers they are also easier to observe and harder to hide ; prefer good old password if possible (for instance as fingerprint fallback option).

 

Small gamedev companies lacks interest in Vulkan

Last month I got interviews for a 3d dev position in a couple of companies near Paris. I mentioned in my resume that I already wrote DX12 and Vulkan code and as expected at some point the interviewers asked me my opinion on DX12 and if I got some performance improvements by using the API. I admitted that my experience is biased since RPCS3 initial GL implementation was not optimal so the performance figure I got were not representative of what can be achieved with DX12.

What surprised me is that my interviewers didn’t show lots of interest in Vulkan. Gamedev studio in Paris can be considered as middle sized ones, between 20 and 70 full time dev who works on several (often niche) titles at the same times for bigger editor. Although they are big enough to maintain their own 3d engine they can’t invest as much money as the big name in the industry. Hence technical choices are often dictated by time and budget constraints.

The first company I was interviewed by (which ships games on PC, PS4 and X1) explained that adding a new rendering backend is costly and that they won’t support Vulkan except if it was the API of the at that time unnamed Nintendo new console (it turns out it’s not the case, the Nintendo Switch is using a custom API, VNM. As far as I know Nintendo always used custom gfx API). With around 1% of market share Linux wasn’t considered as a viable target; neither was Android despite being the first or second most used platform. I suspect the poor state of 3d graphic in the Android ecosystem is to blame here and the web is plenty of horror
story when it comes to OpenGL ES programming. I think that a lot of the enthousiasm surrounding Vulkan comes from the promises of more reliable drivers on Android thanks to the thinner layer of abstraction and the externalization of debug checks. SoC vendors also seems more inclined to improve the situation with Samsung heavily promoting Vulkan support though footage of early demo of Unreal Engine 4 and their partnership with editors to bring Vulkan version of NFS No Limits and Vain Glory on Google Play.

The second company’s engine already has an OpenGL codepath enabling Mac support. While OpenGL and Vulkan are very different in design but they at least share the same shader language (GLSL) which ease any potential porting work (which is still a big task, Vulkan’s being a very verbose API). However, Vulkan was never talked about during the interview; the interviewers were rather interested about what DX12 could bring. The catch is that there’s probably as much work to port a DX11 engine to DX12 as to port it to Vulkan, both Vulkan and DX12 relying on the same gpu abstraction; and while DX12 has a one year head start in term of tool and driver support it’s hindered by the OS support. Although Windows 10 has already gained around 25% of OS market share 60% of the market is still running Windows 7 or 8.x and there isn’t free upgrade offer anymore which makes the adoption rate slower.

On the other hand in both interviews it was clear that support for a low overhead API wasn’t a very high priority. Their engine has made the switch on DX11 very recently to reach parity with PS4 and Xbox One and the dev doesn’t want to reenter a new development cycle right now. At least for Windows; the only way to use Compute Shader, the most popular feature of DX11 hardware gen, on OSX is through Metal API. OpenGL on OSX is supported up to version 4.1 since 2012 and there is no sign that it will change soon. Increasing Metal popularity among will reinforce iOS lead in the smartphone gaming market meaning Apple has no incentive to support the low level API used of their main competitor.

RSX in RPCS3

I’m assuming the reader has some knowledge in graphic programming (with D3D or GL) and generally knows how modern CPU works.

The specs of RSX

RSX is the graphic processor of the PS3. The acronym stands for Reality Synthetiser according to Wikipedia. It’s actually based from Nvidia own Geforce 7800 Gtx, a directX9 class gpu slightly modified to allow Cell’s SPU to do image processing. It has 256 MB of local memory (PS3 terminology for « video memory ») with a 22.4 GB/s bandwidth according to Wikipedia again. It’s processing power is 228 Gflops/s and supports up to 4 render targets.
The aforementioned customisations of RSX allows it to access the main memory (shared by PPU and SPU) at 20 GB/s in read direction and 15 GB/s in write direction. This means that even if it’s slower to render a scene in main memory instead of local memory, the bandwidth hit is rouhly 30%.

Now let’s compare these numbers with the ones from a 2015 PC architecture :
A Geforce 970 has 4 GB of video memory (x16)  with a 200 GB/s bandwidth (x10), can process 5 Teraflop of data (x25) and support 8 render targets. However the theorical peak bandwidth of DD3 is 20 GB/s which is barely what the PS3 did offer in 2007.
The implication for emulation are strong : we can’t afford extra memory transfers between main memory and video memory.

RSX and Cell interaction

In all modern architecture CPU and GPU are executing independently from each others and PS3 is no exception.
RSX commands are 32 bits instructions puts in command buffers in a sequential maneer by Cell. There are 3 special command that are used to break the sequential flow of RSX, namely JUMP (mostly used to move from one command buffer to another) and CALL/RETURN pair (used to implement subroutines). Of course Cell needs to be able to prevent RSX to read commands faster than it can fill command buffer and thus RSX provides a « get » and a « put » register accessible from Cell. « Get » contains the memory address of the command the RSX is currently reading. « Put » can be written to by Cell, and is used as a « barrier », ie the RSX reads command only if Get and Put are different. Put register’s purpose is similar to glFlush in OpenGL.

RSX commands can be sorted in 3 categories :

  • Commands that set RSX register. Like most ancient GPU the RSX doesn’t fetch non buffer inputs in memory but in hardware registers. This includes textures, buffers, render surface… description (their location, their format, their stride, …), vertex constants (RSX has 512 4×32 registers storage for vertex constants), some pipeline state related to blending operation or depth testing. I didn’t mention fragment constants (or pixel shader constant if you prefer D3D terminology) because it looks like there is no true storage for them, the cell has to « patch » fragment program/pixel shader in memory.
  • Commands that issues actual rendering operations. So far I only saw 3 of them, a « clear surface » command that clear render targets (the clear value being stored in register), a « draw » command that issues an unindexed rendering call, an an « indexed draw » command that issues an indexed rendering call.
  • Commands managing semaphores. Semaphore provide a more powerful sync mechanism than the get/put register. Semaphore are basically location in memory associated with a 32 bits values. A wait command can be used to make RSX hold execution until the semaphore values is the same as the expected one, for instance to allow Cell to complete buffer filling task. A release command can be used to make RSX writes a specific value to the semaphore location ; this way a Cell thread can be notified that RSX has finished with a given rendering command and is free to update buffers.