A question about the Access Relation in OpenScop Spec

[李煦阳]

Hi openscop developers!

    I'm currently trying to formalize the polyhedral model and its compilation process (in Coq more precisely). And I check through the openscop spec, in hope that my implementation will be compatible to it.

    There's one thing I encounter: it seems the spec about access relations does not enforce giving the information to relate "array name" and "array identifier", as below, the relation between the array "C" and the array "1".   

             

    "C" identifier is in comment "#", so it may not be provided always. And I know "Array Extension" seems to target to provide this information, but since it's an extension, it may not be provided too.

    These facts lead to my main concern: it seems that without this relation information between "array name" and its "identifier", one is not able to check the consistency between "access relation" and the statement itself within the core of openscop (the access relation gives correct access information as in the statement). Though it does not influence further scheduling or codegen, as I'm doing formal work, this becomes a little problematic, because I wanna check the "consistency". I may wish the core spec contains enough information to check the consistency, like, providing the array name as mandetory.

     

    I'm here to ask whether my concern is tenable, and if it is, is there a way to work this around (since I know changing the spec will lead to compatibility issues, and my work is just a side project)? If it's not, I'll be really very happy to hear your considerations and advice QwQ!

    Thanks in advance!

Best regards, 

Student Xuyang.

      

[Cédric Bastoul]

Hi Xuyang,

nice project! As mentioned in the documentation the first rule of OpenScop design is to "Embed the minimum information to build a complete polyhedral compilation framework in the so-called core part (to avoid as much as possible empty or useless information for each tool)". As you correctly pointed out, the correspondence between the array name and its identifier encoded in the access relation is not necessary for scheduling, hence it's provided only for convenience in an extension. Would it be possible in your work to only consider consistency when this extension is present? Another possibility would be to consider the ordering in which relations are provided to be meaningful (i.e., the first access relation in a statement corresponds to the first array referenced in the statement body). In theory this is not the case, but most tools list accesses in this way and I suppose it is OK to consider stronger consistency.

Note you may have the same issue with statements. Even if most tools suppose statements are provided in the same order as in the original code, only the scattering relation actually encodes the pertinent ordering information. Hence the correspondence with statements is not explicit either.

I fear I'm answering with more problems than solutions, but I hope it helps anyway,

best,

Cedric

--
You received this message because you are subscribed to the Google Groups "OpenSCoP Development" group.
To unsubscribe from this group and stop receiving emails from it, send an email to openscop-develop...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/openscop-development/tencent_31B899F936F5723608D7F4D6%40qq.com.

[李煦阳]

Hi Cedric!

    Many thanks for your quick reply, with really inspiring informations! 

    Your reminder about the inexistence of statements' order information, wakes me that I may not be possible to find a workaround within the core part of openscop, so resorting to the "Array extension" seems to be necessary. And as concretely I'm trying to give PLuTo scheduler a verified validator (therefore formalizing the openscop specification), I may have to complement its openscop with array information (as extension).

    Here's my thoughts: 

    For our first discussion on "array information"'s work around, because I'm trying to give openscop itself a independent consistency definition without considering the access to original C program, it seems that I'm not able to reason out the information even if I preassume the "strong consistency condition" you mention (i.e., the array identifier is related referenced order): the scop has more than one statements, and one specific array may be accessed by multiple statements, so without the original C program (and therefore the order of statements), I have no access to the scop's referenced order. 

     

    Am I omitting something :-D?

    

    Thanks again! 

Best Regards,

Xuyang

 

------------------ Original ------------------

From:  "Cédric Bastoul"<ced...@bastoul.net>;

Date:  Mon, Oct 10, 2022 06:10 AM

To:  "李煦阳"<xuya...@smail.nju.edu.cn>;

Cc:  "openscop-development"<openscop-d...@googlegroups.com>;

Subject:  Re: A question about the Access Relation in OpenScop Spec

[Cédric Bastoul]

Hi Xuyang,

Even with the original C program, you may have different statements with the same text, so only the analysis of the (iteration domains and) scattering functions can tell who is who! But I'm convinced it's not a real issue as you can consider a stronger consistency condition assuming statement and access ordering in the openscop representation is significant (or/and a given extension to be present). A verified validation tool for polyhedral scheduling would be extremely powerful. Any relationship with Courant & Leroy's work https://hal.archives-ouvertes.fr/hal-03000244/document ?

Best,

Cedric

[李煦阳]

Hi Cedric!

    Thanks again! And I'll keep my gratefulness in heart in our further conversation :D

    1. "The strong consistency condition assumption (statement's order and access's order) is enough regardless the access to original C program".   

         Maybe I get your idea now, that, with the assumption in mind, we can always rebuild the order relating array's name and id. 

         This really deepen my understanding. (Though I want to try with explicit extension at the beginning hhh, since this seems more formal and not ad-hoc.)

    2. "My work's relation to Courant & Leroy's POPL'21"

         Yes, I was finding my master thesis's topic (formal verification), and I find this work in POPL'21, with the fact in mind that CompCert is lacking powerful loop optimization passes (especially polyhedral pass), I think integrate a full polyhedral pass, though experimental at first, may be useful. 

         And I examine POPL'21 (it contains only the main part of your codegen algorithm) and the preliminary (and incomplete) polyhedral validation work s2sloop(https://github.com/pilki/s2sLoop) by Pilkiewicz (POPL'21 also mentions this work), I think it seems possible to adapt these work together. 

         I currently think that I have following works to do,  

         i. implement a executable verified validator (using s2sloop's validation strategy), and adapt it to PLuTo main scheduler. I'm on this step now, considering the formalization of openscop itself. 

            What's more, s2sloop gives only a prototype of a validator, lacking a executable constraint solver, I may need to implement it. 

            - I think s2sloop's validation strategy is enough for most scheduling algorithm (without considering efficiency of itself first), because the condition it checks is "full dependence preservation"(all access dependences of Src is preserved by Tgt). And I think correctly implemented algorithm like PLuTo should guarantee it, as it uses the "legality" constraints.   

         ii. I need to connect the three steps (including POPL'21). The extractor seems not difficult (if only deal with "simple" input...). 

         iii. Since polyhedral compilation works on fragments, there needs some work to adapt it to full C program.

          

    Would you mind giving me some comments on my plan's feasibility? :D

Have a nice day,

Xuyang.

 

------------------ Original ------------------

From:  "Cédric Bastoul"<ced...@bastoul.net>;

Date:  Tue, Oct 11, 2022 05:42 AM